[Why3-club] tailor axioms for automatic verification
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
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...
More information about the Why3-club