Email Gateway (Aug 22 2022 at 11:27): Email Gateway (Aug 22 2022 at 11:27):From: Lars Hupel <hupel@in.tum.de>
I'm happy to announce that the Leon system, developed by Viktor Kuncak and
his lab at EPFL, has gained support for Isabelle.
Leon is an automated system for verifying Scala code. You can find more
details on its website [0], try it out online [1], read the sources [2]
and the documentation [3]. In a nutshell, it reads a proper (functional)
subset of Scala and is able to verify assertions in the program. Via
desugaring, it also supports some imperative features. Aside from
verification, it can also find counterexamples (should the assertions not
hold), and attempt to synthesize & repair programs. The underlying proof
obligations are solved with the automated theorem provers Z3 and CVC4.
In the past couple of weeks, Isabelle has been connected to Leon; that is,
proof obligations can be passed to Isabelle, giving users access to the
vast library of mathematical/programming formalisms which are already
available in Isabelle and increasing trustworthiness of the proofs. It is
also possible to convert Scala code into Isabelle code, whereas
previously, only the opposite direction was supported. For this
connection, Makarius' PIDE technology is used (sometimes somewhat
creatively, I have to admit). The work is now fully integrated into Leon.
Here's an example of what can be proven:
@isabelle.proof(method = """(induct "<var xs>", auto)""")
def lemma[A, B, C](xs: List[A], f: A => List[B], g: B => List[C]) =
(xs.flatMap(f).flatMap(g) == xs.flatMap(x => f(x).flatMap(g))).holds
... being the associativity law of the List monad. While this is an
example requiring explicit proof, many other properties can be proven
without an annotation.
Note that in the above snippet, the "method" is an actual Isar proof
method. It is also possible to include larger snippets of theory sources
into Scala sources.
Some technical details are outlined in a presentation [4].
[0] http://lara.epfl.ch/w/leon
[1] http://leon.epfl.ch/
[2] https://github.com/epfl-lara/leon
[3] http://leon.epfl.ch/doc/
[4]
https://speakerdeck.com/larsrh/translating-scala-programs-to-isabelle-with-leon
Last updated: Apr 26 2024 at 01:06 UTC