Email Gateway (Aug 18 2022 at 09:44): Email Gateway (Aug 18 2022 at 09:44):From: Klaus Ostermann <ostermann@informatik.tu-darmstadt.de>
I have seen many examples of proving properties of programming languages (such
as type soundness) in Isabelle.
I wonder whether it is also possible to prove properties of individual programs
written in some language, say Java or C#. It would of course be tiresome to
manually "translate" the program into Isabelle, but in principle it should be
possible to "compile" a Java program into an Isabelle specification, e.g., by
partially evaluating a Java semantics written in Isabelle with an input program.
Has something like this been tried (maybe with another theorem prover)? If yes,
could you give me a reference? If no, are there specific reasons why it has not
been tried?
Regards,
Klaus
Email Gateway (Aug 18 2022 at 09:44):From: Peter Homeier <phomeier@gmail.com>
You may be interested in the Sunrise project. Although not targeting Java
or C#, only a small imperative language similar to a subset of Pascal, it is
a genuine system for proving partial or total correctness of individual
programs written in the Sunrise language, using the Higher Order Logic
theorem prover.
Rather than by translation, which could be considered a "shallow embedding,"
it is based on a "deep embedding" of Sunrise within HOL. Deep embeddings
are much more difficult to create, but once built, have significant
advantages over shallow embeddings.
Please see
http://www.trustworthytools.com/id13.html
Peter
Email Gateway (Aug 18 2022 at 09:45):From: Tobias Nipkow <nipkow@in.tum.de>
The compilation approach (without partial evaluation) has been used in
at least two systems: the Loop tool by Huisman, Jacobs et al, and the
Jive system by Mueller, Poetzsch-Heffter and Rauch.
Tobias
Klaus Ostermann schrieb:
Email Gateway (Aug 18 2022 at 09:46):From: Norbert Schirmer <norbert.schirmer@web.de>
Hello Klaus Ostermann,
as part of the Verisoft project (www.verisoft.de) I have developed a
verification environment for sequential imperative programs over the last few
years. It's a combination of a deep and shallow embedding and provides a
quite general core language that is suitable to express most common language
constructs of imperative programming languages. Allthough the focus in
Verisoft is on a subset of C, I believe it can also be customized to express
the object-oriented features of languages like Java or C#. I look forward to
someone heading in this direction. So if you are interested have a look at:
http://www4.in.tum.de/~schirmer/verification_environment.html
Norbert
Email Gateway (Aug 18 2022 at 09:50):From: Primrose.Mbanefo@Infineon.com
I work on the proof of properties of programs in SystemC (a c++ class library) and use the compilation approach (with shallow embedding). The work is quite preliminary and still has no external references to it.
But an overview of deep/shallow embeddings can be found in:
Azurat, A. & Prasetya, I.
A survey on Embedding Programming logics in a Theorem Prover
Inst. of Information and Comp. Science, Utrecht Univ., 2002
Tech report: UU-CS-2002-007
You can, in addition to extending Norberts sequential environment, also consider compiling towards an already existing java embedding (which might most likely need some extending too):
von Oheimb, D.
Analyzing Java in Isabelle/HOL-Formalization, Type Safety and Hoare Logic
Ph.D. thesis, Technische Universität München, 2001
Regards,
Primrose
Last updated: May 03 2024 at 08:18 UTC