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

PVS questions



Hello !

One question about array.

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?
(2) If I need to use/quote/reference a_2 and b_2 separately, how can I
do 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?

Thank you for your help.

Pu Zhang