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

Re: Correction : problem with WITH (ignore earlier mail)



Tamarah Arons wrote:
> 
> Correction:
> 
> Sorry, in the last mail I accidentally added an extra ``message'' field to
> the last sequent when I was cutting and pasting. It didn't belong.
> 
> The, whole, corrected question is below.
> 
> Sorry, again!
> 
> Tamarah
> __________________________________________________________________
> 
> Hello,
> 
> I have a consequent, which I think should be trivial to prove,
> but I have not succeeded. I have tried simplify, (assert :flush? t),
> whatever I could think of, but to no avail.
> 
> The consequent is
> 
>  |-------
> [1,(idPCunique)]
>       id(cEntry!1) =
>        id(cEntry!1
>             WITH [v := mem!1(a(cEntry!1)),
>                   t := t(procs!1(0))])
> 
> where cEntry!1 is of type [# v : VALUE, t : TIME,
>                              id : PROC_ID, pc : PC_RANGE#]
> 
> Since the id field is not modified by the WITH statement I would expect
> the proof to be simple.
> 
> Trying (grind) I get an unprovable sequent as follows:
> 
> id rewrites id(cEntry!1)
>   to cEntry!1
> id rewrites
>   id(cEntry!1
>        WITH [v := mem!1(a(cEntry!1)), t := t(procs!1(0))])
>   to cEntry!1
>         WITH [v := mem!1(a(cEntry!1)), t := t(procs!1(0))]
> Trying repeated skolemization, instantiation, and if-lifting,
> this simplifies to:
> idPCunqiue 5.1 :
> 
>   |-------
> {1,(idPCunique)}
>       cEntry!1 =
>        cEntry!1
>          WITH [v := mem!1(a(cEntry!1)), t := t(procs!1(0))]
> 
> Any suggestions would be appreciated.
> 
> Thanks,
> Tamarah
> 
> P.S. I am using PVS 2-3 no patches

There's a function "id" in the PVS prelude that's defined
as the identity function. That's the one PVS picks in your 
sequent rather than the "id" field of the structure "cEntry!1". 
Try using the syntax "cEntry!1`id" rather than "id(cEntry!1)".
That should solve your problem.

Bruno

-- 
Bruno Dutertre                             | bruno@sdl.sri.com
SDL, SRI International                     | fax: 650 859-2844
333 Ravenswood Avenue, Menlo Park CA 94025 | tel: 650 859-2717