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

PVS Bug 1033


Synopsis:        simple proof crashes PVS4.1 with "simple-error"
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Thu Mar 27 09:20:01 -0700 2008
Originator:      Rick Butler
Release:         PVS 4.1
Organization:    nasa.gov
Environment: 
 System:          
 Architecture: 

Description: 
  --Boundary-00=_QA76HAgWz63bhNy
  Content-Type: text/plain;
    charset="us-ascii"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline
  
  safe_prop :  
  
    |-------
  {1}   FORALL (B: bool, x: nat): f(x, B) >= g(x) * h(B)
  
  Rule? (skosimp*)
  Repeatedly Skolemizing and flattening,
  this simplifies to: 
  safe_prop :  
  
    |-------
  {1}   f(x!1, B!1) >= g(x!1) * h(B!1)
  
  Rule? (lemma "f")
  Applying f 
  this simplifies to: 
  safe_prop :  
  
  {-1}  f = (LAMBDA (x, B): IF x > 30 AND B THEN x * x ELSE 90 * x ENDIF)
    |-------
  [1]   f(x!1, B!1) >= g(x!1) * h(B!1)
  
  Rule? (replace -1)
  Replacing using formula -1,
  this simplifies to: 
  safe_prop :  
  
  [-1]  f = (LAMBDA (x, B): IF x > 30 AND B THEN x * x ELSE 90 * x ENDIF)
    |-------
  {1}   (LAMBDA (x, B): IF x > 30 AND B THEN x * x ELSE 90 * x ENDIF)
            (x!1, B!1)
         >= g(x!1) * h(B!1)
  
  Rule? (assert)
  Error: the assertion
         (subsetp (freevars preds)
                  (union (freevars ex) *bound-variables*)
           :key #'declaration)
         failed.
    [condition type: simple-error]
  
  Restart actions (select using :continue):
   0: retry assertion.
   1: Return to Top Level (an "abort" restart).
   2: Abort entirely from this (lisp) process.
  [1] pvs(28): 
  
  --Boundary-00=_QA76HAgWz63bhNy
  Content-Type: text/plain;
    charset="us-ascii";
    name="demo_recur.pvs"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: attachment;
  	filename="demo_recur.pvs"
  
  demo_recur: THEORY
  %----------------------------------------------------------------------------
 -%
  %   									      %
  %   			  |--------------|                                    %
  %   			  |              |  -->  f(x,B)                       %
  %   		   x -->  |              |                                    %
  %   			  |              |  -->  g(x)                         %
  %   			  |              |                                    %
  %   		   B -->  |              |  -->  h(B)                         %
  %   			  |              |                                    %
  %   			  |--------------|                                    %
  %   									      %
  %----------------------------------------------------------------------------
 -%
  BEGIN
  
     x: VAR nat
     B: VAR bool
   
     f(x,B): nat = IF x > 30 AND B THEN x*x ELSE 90*x ENDIF
  
     g(x): RECURSIVE real = 
                   IF x >= 10 THEN g(x-10) + x/5 ELSE 0 ENDIF
                   MEASURE x
  
     h(B): nat   = IF B THEN 40 ELSE 0 ENDIF
  
  
  
     safe_prop: LEMMA f(x,B) >= g(x) * h(B)
  
  
  
  
  %----------------------------------------------------------------------------
 -%
  %   									      %
  %      x   |   B           f    |     g    |   h              safe_prop
  %     -----|------       ----------------------------       ------------
  % 	0  |   T           0    |     0    |  60                TRUE
  %      10  |   F          1200  |    20    |   0                TRUE
  %      50  |   T          2500  |     0    |  60                TRUE
  %      30  |   F          3600  |    60    |   0                TRUE
  %      30  |   T          3600  |    60    |  60                TRUE
  %
  %----------------------------------------------------------------------------
 -%
  
  END demo_recur
  
  --Boundary-00=_QA76HAgWz63bhNy--

How-To-Repeat: 

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