Re: PVS questions

[Dave Stringer-Calvert <dave_sc@csl.sri.com>]

> For instance, I want to define an array S containing 50 elements. Each
> element is a tuple/record in the form (a, b). Suppose S={(a_1,b_1),
> (a_2,b_2), ... , (a_50, b_50)}
> 
> (1) How to define such an array using PVS?

You could use either the tuple or record constructs:

   A_TYPE, B_TYPE : TYPE+

   % Tuple version
   S_TYPE : TYPE = [below(50) -> [A_TYPE, B_TYPE]]

   % Record version
   S_TYPE : TYPE = [below(50) -> [# a : A_TYPE, b : B_TYPE #]]


below() is defined in the PVS prelude (view it using M-x vpf) as a subtype
of the natural numbers, so below(50) is the type of the range 0...49.


> (2) If I need to use/quote/reference a_2 and b_2 separately, how can I 
>  that? I'm   afraid that I cannot reference them in C style such as
> S[2].a and S[2].b, so how can I do that in  PVS?

There are several syntactic forms available.  Here are some examples
for both the tuple and record methods:

   s : S_TYPE

   % Tuple version
   an_a : A_TYPE = s(2)`1
   another_a : A_TYPE = proj_1(s(2))
 

   % Record version
   an_a      : A_TYPE = s(2)`a
   another_a : A_TYPE = a(s(2))


You'll find all this documented, with examples, in the PVS language
reference manual at http://pvs.csl.sri.com/manuals.html

Dave