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

Re: FIELDS bug in grind



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