[Why3-club] error in importing real at Abs into PVS file
dragan.stosic at gmail.com
Wed Nov 20 13:28:27 CET 2013
I am using the following :
1) The Ocaml version 3.12.1
2) Coq Proof Assistant, version 8.3pl4
3) The frama-c-Fluorine-20130601
4) The Prototype Verification System PVS version 6.0 with nasalib-6.0.5
5) The why-2.33
6) The why3 version from git - one month ago.
I have tried bsearch algorithm from acsl-implementation-Fluorine-20130601
and PVS failed on type checking.
The following importing clauses can be seen in the PVS file :
IMPORTING int at Int
IMPORTING int at Abs
IMPORTING int at ComputerDivision
IMPORTING floating_point at Rounding
IMPORTING real at Real
* IMPORTING real at Abs1*
IMPORTING real at FromInt
IMPORTING floating_point at SingleFormat
IMPORTING floating_point at DoubleFormat
IMPORTING floating_point at Single
IMPORTING floating_point at Double
However, Abs1 does not exist in the pvs library provided by why3.
After correction to Abs, type checking passed successfully.
Senior developer at IBM
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Why3-club