[Why3-club] error in importing real at Abs into PVS file

Dragan dragan.stosic at gmail.com
Wed Nov 20 13:28:27 CET 2013

Hi all,
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.


Dragan Stosic
Senior developer at IBM
phone: 085-773-1050
e-mail: dragan.stosic at gmail.com
e-mail:DRAGANST at ie.ibm.com
IBM Technology Campus
Damastown Industrial Estate
Dublin 15
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131120/32773f26/attachment.html>

More information about the Why3-club mailing list