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:
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