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

Re: [PVS-Help] Records and quantifying over fields



Thanks, Sam,

Paul Miner already suggested this, and I tried it yesterday - I think it 
looks like that is indeed the better choice.


Hanne


Sam Owre wrote:
> Hi Hanne,
> 
> It is not allowed to quantify over fields in general.  It makes sense
> for this record type, but in general records have fields of different
> types, in which case the variable cannot be given a type (unless, as in
> some type systems, there is a "top" type).  I think you would be better
> off with an array, or you could do something like
> 
>   PosName: TYPE = {p11, p12, p13, p21, p22, p23, p31, p32, p33}
>   World: TYPE = [PosName -> Position(3)]
> 
> then for a World w, you could say
>   
>   exists (p, q: PosName): w(p) = w(q)
> 
> I hope this helps.
> Sam
>   
> 
> Hanne Gottliebsen <hago@dcs.qmul.ac.uk> wrote:
> 
>> If I  have a record type (and constants of that type), is it possible to
>> quantify over the fields?
>>
>> World : TYPE = [# p11, p12, p13,
>>                    p21, p22, p23,
>>                    p31, p32, p33: Position(3) #]
>>
>> Given a world, w, I would like to say something like
>>
>> exists (p,q: positions in w) : p = q
>>
>> (Actually, what I want to say about p and q is more complicate, but I
>> think this is enough to explain my problem).
>>
>> Is this possible? Or should I be looking at another type (array maybe) in
>> the first place?
>>
>>
>> Thanks,
>> Hanne
>> -- 
>> ---------------------------------------------------------
>> Dr. Hanne Gottliebsen    Department of Computer Science
>> hago@dcs.qmul.ac.uk      Queen Mary, University of London
>> Ph: +44 (0) 207 882 5259
>>    - I want a single-skin cotton tent like Mr Weasley's
>> ---------------------------------------------------------


-- 
---------------------------------------------------------
Dr. Hanne Gottliebsen    Department of Computer Science
hago@dcs.qmul.ac.uk      Queen Mary, University of London
Ph: +44 (0) 207 882 5259
   - I want a single-skin cotton tent like Mr Weasley's
---------------------------------------------------------