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

Re: FIELDS bug in grind



Sam,

  Yes, that fixed it. I did not realize I was running an old version!
Thanks so much.

-eric

On Tue, 30 Apr 2002, Sam Owre wrote:

> Hi Eric,
>
> I tried to recreate this bug in version PVS 2.4, but (grind)
> worked correctly there.  I then did manage to recreate the bug
> in PVS 2.3.  So I would suggest you upgrade to the latest
> version of PVS, and let me know if that's a problem for you.
>
> Thanks,
> Sam Owre
>
> > Hi,
> >
> >   When I use (grind) to try to prove "simple1" below, the prover gives an
> > error (see the comments before declaration of "simple1"). If I (expand
> > ...) all the definitions, (grind) works fine.
> >
> >   I have tried to make the example small to help you in finding the bug --
> > but I have not narrowed down the expact part of the theory below that
> > causes the error.
> >
> >   If you have an easy fix for this, please let me know.
> >
> >   Cheers,
> >
> >   -eric
> >
> > P.S. I love PVS.
> >
> >            o----
> >            | Eric Klavins
> >            | Postdoctoral Scholar
> >              Caltech Computer Science
> >              klavins@cs.caltech.edu
> >              (626)395-4858
> >
> > --------------------------------------------------------------------------------------
> >
> > bug: THEORY
> >
> >   BEGIN
> >
> >     value : TYPE = [# int_val : int, real_val : real #]
> >     state : TYPE = [ s : string -> value ]
> >
> >     guard :		TYPE = [state -> bool]
> >     rule  :		TYPE = [state, state -> bool ]
> >     clause :		TYPE = [# g : guard, r : rule #]
> >     program :		TYPE = [# init : guard, clauses : set [ clause ] #]
> >
> >     app ( p : program, s : state ) : set [ clause ] =
> >       { c : clause | member ( c, p`clauses ) AND c`g ( s ) }
> >
> >     simply_follows? ( p : program, s1 : state, s2 : state ) : bool =
> >       FORALL ( c : clause ) : ( member ( c, app ( p, s1 ) ) => c`r ( s1, s2 ) )
> >
> >     p1 : program = (#
> >       init := lambda ( s : state ) : true,
> >       clauses := singleton (
> >         (#
> >            g := lambda ( s : state ) : true,
> >            r := lambda ( s1 : state, s2 : state ) : s2("a")`int_val = s1("a")`int_val + 1
> >          #)
> >       )
> >     #)
> >
> >     s ( n : nat )  : state  = lambda ( v : string ) : (# int_val := n, real_val := 0 #)
> >
> >     %
> >     % tring to prove the theorem "simple1" with (grind) results in
> >     %
> >     % simple1 :
> >     %
> >     %  |-------
> >     % {1}   simply_follows?(p1, s(0), s(1))
> >     %
> >     % Rule? (grind)
> >     % Error: No methods applicable for generic function
> >     %       #<STANDARD-GENERIC-FUNCTION FIELDS> with args (s: string) of
> >     %       classes (DEP-BINDING)
> >     %  [condition type: PROGRAM-ERROR]
> >     %
> >     % Restart actions (select using :continue):
> >     %  0: Try calling it again
> >     %  1: Return to Top Level (an "abort" restart)
> >     % [1c] PVS(105):
> >
> >     simple1 : THEOREM
> >       simply_follows? ( p1, s(0), s(1) )
> >
> >   END bug
>