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.
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