[Why3-club] Problems when handling arrays from Why3 theory files

Santiago Saavedra s.saavedra at fdi.ucm.es
Mon Oct 10 18:52:12 CEST 2016


Dear why3-club folks,

I'm trying to use Why3 to discharge formulae built in .why format for
a research platform (we wanted to generate the verification conditions
ourselves). However, I found out that when code used arrays, our
generated why code does not properly discharge against SMT solvers,
whilst if we use WhyML to construct a similar proof, then the proof is
discharged.

I found out that when your VCGen encounters an array, three different
declarations are performed (one for each field in the array record,
namely the length and a map containing the elements, and one for the
array proper as a call to the Mk_array constructor).

However, when using our goals, the generated tasks do not include the
additional maps and lengths as different elements (and thus,
invariants on the data type such as a.length >= 0 are not inferred).

Also, it seems that the generated task theory is not a valid Why3
file, as it includes definitions which seem to be hardwired on Why3,
such as the array get/set syntax or the integers theory.

We were wondering which is the proper way to handle arrays as why
theory files, and if support for such a feature should be beneficial
to include in Why3 or would need some workaround.


Kind regards,

-- 
Santiago Saavedra
Dept. Sistemas Informáticos y Computación
Faculty of Computer Science
C/ Prof. José García Santesmases, 9
Complutense University of Madrid, 28040 Madrid
Tlf.: +34 91 394 7648 | email: s.saavedra at fdi.ucm.es


More information about the Why3-club mailing list