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
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
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:
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
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: Nov 21 2024 at 12:39 UTC