Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions



> At the danger of being called a nitpicker: this sort of thing can cost
> you the programme correctness that you have so painstakingly ensured
> with Isabelle, since Int in Scala is subject to integer overflow. I have
> heard stories of "verified" code producing horribly wrong results
> because people did not take integer overflow into account. These stories
> were from code verified with a verification condition generator and
> automated theorem provers; the Isabelle-generated code is, of course,
> not affected by things like this, but when writing wrappers around it
> that use native integer types, the same caveats apply.
> 
> Personally, unless I do some heavy number-crunching, I use the
> arbitrary-precision Integer type (in Haskell) just to be sure –
> especially with Isabelle-generated code.

Interfacing with generated code requires indeed some care.  E.g. the
generated code does not prevent you from generating abstract values
which do not obey the required invariant.  Clean encapsulated interfaces
are helpful here.

	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

Attachment: signature.asc
Description: OpenPGP digital signature



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