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

[PVS-Help] ELSE clause in CASES

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
      % Ensure this input matches the return type                                                                                                                                                       
      % Ensure this input matches the return type                                                                                                                                                       
      % Ensure this input matches the return type                                                                                                                                                       

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.)

Ben Hocking