Re: [isabelle] small verification task

You cannot (yet) verify SML code directly. But you can translate it by hand into HOL and verify the result. See HOL/Library/GCD.thy for an example.


Joao Marcos schrieb:
Dear All:

Is it possible to write a small piece of code in SML, say, to compute
the GCD of 2 given numbers, and use Isabelle and its induction tactic
to directly verify the correctness of this very code?  Anyone would
kindly point to examples where this has been done?


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.