*To*: Manuel Eberl <eberlm at in.tum.de>*Subject*: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions*From*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Date*: Fri, 05 Jul 2013 19:32:46 +0200*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <51D4A7E7.1000109@in.tum.de>*Organization*: TU Munich*References*: <51D3205A.5030303@gmail.com> <51D46E5F.7000804@informatik.tu-muenchen.de> <51D49B99.20408@gmail.com> <51D4A7E7.1000109@in.tum.de>*User-agent*: Mozilla/5.0 (X11; Linux i686; rv:17.0) Gecko/20130623 Thunderbird/17.0.7

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

**References**:**[isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions***From:*Christoph LANGE

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

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

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

- Previous by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Date: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Previous by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Next by Thread: Re: [isabelle] Scala code generator generates ill-typed code from subtraction of n-ary functions
- Cl-isabelle-users July 2013 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list