[Why3-club] [Q612-030] adapt SPARK to Why3 1.0.0

Andrei Paskevich andrei.paskevich at lri.fr
Wed Jul 25 22:01:53 CEST 2018


On 25 July 2018 at 21:55, Yannick Moy <moy at adacore.com> wrote:
>> This is also on purpose: the tt'int operation is used for
>> specification purposes, if you make it non-ghost, you would need to
>> link the extracted code with an arbitrary-precision arithmetic
>> library.
>
> so type "int" is also ghost? we might need to mark all the generated Why3
> code as ghost then.

There is no such thing as ghost type in Why3 :)

No, the operations on int are non-ghost, so that you can still write a
program on mathematical integers without making everything ghost.
However, we consider that once you start using bounded integers, you
intend your program for efficient execution, and thus unbounded ints
are assumed to be specification only. If you want to combine range
ints and unbounded ints in the same non-ghost code, just define a
plain "val int_of_tt (x: tt) : int ensures { result = tt'int x }" and
use it instead of tt'int.

Andrei


More information about the Why3-club mailing list