[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] ELSE clause in CASES



Ben,

There is no comma before ELSE and no colon after it.



Cesar
--
Cesar A. Munoz, NASA <Cesar.A.Munoz@xxxxxxxx>
Web: http://shemesh.larc.nasa.gov/people/cam
NASA Langley Research Center, Bldg. 1220, Room 115 MS. 130, Hampton, VA
23681-2199, USA
Office: +1 (757) 864 1446. Fax: +1 (757) 864 4234






On 10/23/14 12:04 PM, "Ben Hocking" <benjaminhocking@xxxxxxxxx> wrote:

>Hi all,
>
>
>I have a question about the PVS language (6.0).
>
>
>Per the PVS language reference
>(http://pvs.csl.sri.com/doc/pvs-language-reference.pdf): "The CASES
>expression also allows an ELSE clause, which comes last and covers
> all constructors not previously mentioned in a pattern.²
>
>
>According to PVS, ³Found 'ELSE' when expecting '!id!, Š lots of other
>things, but not ELSE Š², when examining the following function:
>Data_Type_Duplicate(p_Constant: int32, p_In1: int32, p_In2: int32, dummy:
>int): int32
>
>=
>  
>CASES dummy 
>OF
>    0:
>     
>% Ensure this input matches the return type
>                  
>                  
>      p_Constant,
>    1:
>     
>% Ensure this input matches the return type
>                  
>                  
>      p_In1,
>    
>ELSE:
>     
>% Ensure this input matches the return type
>                  
>                  
>      p_In2
> 
>ENDCASES
>
>
>
>I tried the ELSE with and without the ³:², but PVS rejects both. Am I
>doing something wrong, or is the language reference wrong? Note that I
>examined several CASES in the NASA libraries and none of them used the
>ELSE clause. (As a very minor side
> point, note that incorrect coloring of ³Type² in ³Data_Type_Duplicate²
> - the PVS environment has some minor flaws in its syntax highlighting.
>This happens when any keyword is part of a variable or function name.)
>
>
>Thanks,
>Ben Hocking
>benjaminhocking@xxxxxxxxx
>
>
>
>
>