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

# PVS Bug 769

```Synopsis:        Unexpected restrict of numfield type
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri May  2 16:40:01 2003
Originator:      Alfons Geser
Organization:    shrimp.nianet.org
Release:         PVS 3.1
Environment:
System:
Architecture:

Description:
Hi,

an unexpected "restrict" is produced in PVS 3.1. The code works
perfectly with PVS 2.4.

Alfons

---

Attempting to prove lemma t1 by

(skosimp*) (expand "form_set") (expand "singleton") (assert)

produces the sequent

[-1]  restrict[[# te: numfield, ve: Vect3, vr: Vect3 #], solution, boolean]
({y: [# te: numfield, ve: Vect3, vr: Vect3 #] |
y =
(# ve := put_z(v!1, vez!1),
vr := put_z(v!1, vrz!1),
te
:= (v!1(2) * tr!1 - tr!1 * vrz!1) / (vez!1 - vrz!1) #)})
(m!1)
|-------
{1}   m!1 =
(# ve := put_z(v!1, vez!1),
vr := put_z(v!1, vrz!1),
te := (v!1(2) * tr!1 - tr!1 * vrz!1) / (vez!1 - vrz!1) #)

which seems unprovable.  If "singleton" is qualified by "[solution]"
(as in the commented line) then the proof works.

---

%% Unexpected restrict of numfield type

restrict_bug: THEORY
BEGIN

IMPORTING vectors@vect3D

solution : TYPE = [# ve: Vect3, vr:Vect3, te:real #]

v   : VAR Vect3
tr, te, vez, vrz  : VAR real
m   : VAR solution

form_set(v, vez, vrz, tr) : set[solution] =
%        singleton((# ve:= put_z(v, vez),
singleton[solution]((# ve:= put_z(v, vez),
vr:= put_z(v, vrz),
te:= tr*(z(v) - vrz)/(vez-vrz) #))

t1 : LEMMA
form_set(v, vez, vrz, tr)(m)
IMPLIES
m = (# ve:= put_z(v, vez),
vr:= put_z(v, vrz),
te:= tr*(z(v) - vrz)/(vez-vrz) #)

END restrict_bug

How-To-Repeat:

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