Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 446


Synopsis:        problem with the abstract-and-mc command
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Sun Mar 12 12:20:00 2000
Originator:      rusu
Organization:    irisa.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------2D140CE27BBF091A74FD7FE3
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  
   Hi,
  
   I think there are some problems with the abstract-and-mc command.
  With the attached file (it's one of the examples you showed at FM),
  when trying to "prove" the theorem "prop" with the command
  
   (abstract-and-mc ("LAMBDA (s: State) : TRUE"))
  
  I get: Error: No methods applicable for generic function
         #<STANDARD-GENERIC-FUNCTION DECLARATION> with args (NIL) of
         classes (NULL)
    [condition type: PROGRAM-ERROR]
  
  Also, the abstraction command with just one predicate
  
  (abstract-and-mc ("LAMBDA (s: State) : B(s) = 0"))
  
  succeeds in proving the theorem. This is strange, because
  the abstract system is too coarse to prove anything here...
  
   Regards,
  
   Vlad
  --------------2D140CE27BBF091A74FD7FE3
  Content-Type: text/plain; charset=us-ascii;
   name="even.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="even.pvs"
  
  even 	: THEORY
  
    BEGIN
  
     PCtype: TYPE = {inc, dec}
  
     State: TYPE = [# PC : PCtype,
                     B: int #]
  
  
     s, s0, s1: VAR State
     i, j, k: VAR nat
  
     init(s): bool =
      (PC(s) = inc AND
       B(s) = 0)
  
     next0(s0, s1): bool =
      (PC(s0) = inc AND
       B(s1) = B(s0) + 2 AND 
       PC(s1) = dec)
  
     next1(s0, s1): bool =
      (PC(s0) = dec AND
       B(s0) > 0 AND
       B(s1) = B(s0) - 2) % PC(s1) unconstrained
  
     next(s0, s1): bool =
      (next0(s0, s1) OR next1(s0, s1))
  
     inv1(s): bool = (B(s) >= 0)
  
     prop: THEOREM
      init(s) IMPLIES AG(next, inv1)(s)
  
    END even
  
  
  
  
  
  
  
  
  
  
  
  
  
  --------------2D140CE27BBF091A74FD7FE3--

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools