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

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



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