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

Re: [PVS-Help] ELSE clause in CASES



Thank you (and Cesar) for your clear help. I fixed that and now get the error message, "_expression_ type must be a cotuple or datatype”, referring to dummy, which is an int. Per the language guide, “The CASES _expression_ uses a simple form of pattern-matching on abstract datatypes,” so clearly I was using CASES wrong.

I’ve gone with an IF…ELSIF…ENDIF instead.

Thanks again for your help,

On Oct 23, 2014, at 3:49 PM, Di Vito, Benedetto L. (LARC-D320) <b.divito@xxxxxxxx> wrote:

Ben,

The syntax you need is to drop both the colon after ELSE and the preceding comma:

  CASES dummy OF  0: p_Constant,  1: p_In1  ELSE p_In2  ENDCASES

Regards,
Ben



From: Ben Hocking <benjaminhocking@xxxxxxxxx>
Date: Thursday, October 23, 2014 12:04 PM
To: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>
Cc: Michael Anthony Aiello <tony.aiello@xxxxxxxxxxxxxxxxxxxxxxx>
Subject: [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
    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,