Re: [isabelle] small verification task



Exactly this (and quite a lot more - ML definitions of datatypes as well as functions) was possible in the LAMBDA prover, marketed by Abstract Hardware Limited in the 80s and 90s.

N. Chapman, S. Finn, and Michael P. Fourman. Datatypes in L2. In T.F. Melham and J. Camillieri, editors, Higher Order Logic Theorem Proving and its Applications. 7th International Workshop Proceedings, pages 128-43, Valetta, Malta, September 1994. Springer-Verlag; Berlin, Germany. Invited Paper.

Simon Finn, Michael P. Fourman, and John Longley. Partial functions in a total setting. J. Automated Reasoning, 18(1):85-104, 1997. Zbl. 0870.68136.

Michael

On 16 Sep 2007, at 18:46, Tobias Nipkow wrote:

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.

Tobias

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?
Best,
JM




Michael P. Fourman FBCS CITP School of Informatics Professor of Computer Systems Appleton Tower, Crichton Street Head of Informatics Edinburgh EH8 9LE The University of Edinburgh Scotland UK
http://www.inf.ed.ac.uk/
For diary entries contact Alex.Judd at ed (etc.)      +44 131 650 2690






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