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

FIELDS bug in grind



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