[Why3-club] tailor axioms for automatic verification

Cláudio Amaral coa at dcc.fc.up.pt
Thu Nov 7 14:22:17 CET 2013


I am trying to encode some features in Why3 that are described with
higher-order functions.

It seems Why does not have the expressive power in the type description to
directly use first class functions (happy to be wrong here :-) so I decided
to mimic the higher order with a 'run' function (monadic inspired) and
axiomatize the behaviour.

My 'problem' is that I have two families of axiom for the same set of
functions: simplification of specific applications (true and a = a, for
example) and the execution of the function performed by 'run' (f(x) = (y,
state_information), for example).

Should I put all the axioms in the specification of 'run' or the provers
will not discriminate if I have the simplification axioms not related to
'run' at all?

Also, how should I force the direction of an equality if I have some
rewrite rules  I want to apply?

A third subject, has anyone implemented any kind of monadic theories or
used monads in Why3?

Thanks in advance
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/why3-club/attachments/20131107/8974b698/attachment.html>

More information about the Why3-club mailing list