Iteratively Composing Statically Verified Traits

Isaac Oscar Gariano
Marco Servetto
Alex Potanin
Hrshikesh Arora

Static verification relying on an automated theorem prover can be very slow and brittle: since static verification is undecidable, correct code may not pass a particular static verifier. In this work we use metaprogramming to generate code that is correct by construction. A theorem prover is used only to verify initial "traits": units of code that can be used to compose bigger programs.

In our work, meta-programming is done by trait composition, which starting from correct code, is guaranteed to produce correct code. We do this by extending conventional traits with pre- and post-conditions for the methods; we also extend the traditional trait composition (+) operator to check the compatibility of contracts. In this way, there is no need to re-verify the produced code.

We show how our approach can be applied to the standard "power" function example, where metaprogramming generates optimised, and correct, versions when the exponent is known in advance.

In Alexei Lisitsa and Andrei Nemytykh: Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019), Genova, Italy, 2nd April 2019, Electronic Proceedings in Theoretical Computer Science 299, pp. 49–55.
Published: 20th August 2019.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: