Iteratively Composing Statically Verified Traits

Isaac Oscar Gariano; Marco Servetto; Alex Potanin; Hrshikesh Arora

doi:10.4204/EPTCS.299.7

Iteratively Composing Statically Verified Traits

Isaac Oscar Gariano, Marco Servetto, Alex Potanin, Hrshikesh Arora

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

Abstract

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.

Original language	English
Title of host publication	Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019)
Editors	Alexei Lisitsa, Andrei Nemytykh
Place of Publication	Genova, Italy
Publisher	Electronic Proceedings in Theoretical Computer Science
Pages	49-55
Number of pages	7
DOIs	https://doi.org/10.4204/EPTCS.299.7 https://doi.org/10.4204/EPTCS.299.7
Publication status	Published - 20 Aug 2019
Externally published	Yes
Event	7th International Workshop on Verification and Program Transformation, VPT 2019 - Genova, Italy Duration: 2 Apr 2019 → 2 Apr 2019 https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?VPT2019 http://dx.doi.org/10.4204/EPTCS.299

Publication series

Name	Electronic Proceedings in Theoretical Computer Science, EPTCS
Publisher	Open Publishing Association
Volume	299
ISSN (Print)	2075-2180

Conference

Conference	7th International Workshop on Verification and Program Transformation, VPT 2019
Country/Territory	Italy
City	Genova
Period	2/04/19 → 2/04/19
Internet address	https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?VPT2019 http://dx.doi.org/10.4204/EPTCS.299

Access to Document

Cite this

Gariano, I. O., Servetto, M., Potanin, A., & Arora, H. (2019). Iteratively Composing Statically Verified Traits. In A. Lisitsa, & A. Nemytykh (Eds.), Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019) (pp. 49-55). (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 299). Electronic Proceedings in Theoretical Computer Science. https://doi.org/10.4204/EPTCS.299.7, https://doi.org/10.4204/EPTCS.299.7

Gariano, Isaac Oscar ; Servetto, Marco ; Potanin, Alex et al. / Iteratively Composing Statically Verified Traits. Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019). editor / Alexei Lisitsa ; Andrei Nemytykh. Genova, Italy : Electronic Proceedings in Theoretical Computer Science, 2019. pp. 49-55 (Electronic Proceedings in Theoretical Computer Science, EPTCS).

@inproceedings{e8ce00a0abc9495abe5b6112189d146f,

title = "Iteratively Composing Statically Verified Traits",

abstract = "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.",

author = "Gariano, \{Isaac Oscar\} and Marco Servetto and Alex Potanin and Hrshikesh Arora",

note = "Publisher Copyright: {\textcopyright} I. O. Gariano, M.,Servetto, A. Potanin \& H. Arora.; 7th International Workshop on Verification and Program Transformation, VPT 2019 ; Conference date: 02-04-2019 Through 02-04-2019",

year = "2019",

month = aug,

day = "20",

doi = "10.4204/EPTCS.299.7",

language = "English",

series = "Electronic Proceedings in Theoretical Computer Science, EPTCS",

publisher = "Electronic Proceedings in Theoretical Computer Science",

pages = "49--55",

editor = "Alexei Lisitsa and Andrei Nemytykh",

booktitle = "Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019)",

url = "https://cgi.cse.unsw.edu.au/\textasciitilde{}eptcs/content.cgi?VPT2019, http://dx.doi.org/10.4204/EPTCS.299",

}

Gariano, IO, Servetto, M, Potanin, A & Arora, H 2019, Iteratively Composing Statically Verified Traits. in A Lisitsa & A Nemytykh (eds), Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019). Electronic Proceedings in Theoretical Computer Science, EPTCS, vol. 299, Electronic Proceedings in Theoretical Computer Science, Genova, Italy, pp. 49-55, 7th International Workshop on Verification and Program Transformation, VPT 2019, Genova, Italy, 2/04/19. https://doi.org/10.4204/EPTCS.299.7, https://doi.org/10.4204/EPTCS.299.7

Iteratively Composing Statically Verified Traits. / Gariano, Isaac Oscar; Servetto, Marco; Potanin, Alex et al.
Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019). ed. / Alexei Lisitsa; Andrei Nemytykh. Genova, Italy: Electronic Proceedings in Theoretical Computer Science, 2019. p. 49-55 (Electronic Proceedings in Theoretical Computer Science, EPTCS; Vol. 299).

Research output: Chapter in Book/Report/Conference proceeding › Conference Paper › peer-review

TY - GEN

T1 - Iteratively Composing Statically Verified Traits

AU - Gariano, Isaac Oscar

AU - Servetto, Marco

AU - Potanin, Alex

AU - Arora, Hrshikesh

N1 - Publisher Copyright: © I. O. Gariano, M.,Servetto, A. Potanin & H. Arora.

PY - 2019/8/20

Y1 - 2019/8/20

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85072224132

UR - https://cgi.cse.unsw.edu.au/~eptcs/content.cgi?VPT2019

U2 - 10.4204/EPTCS.299.7

DO - 10.4204/EPTCS.299.7

M3 - Conference Paper

AN - SCOPUS:85072224132

T3 - Electronic Proceedings in Theoretical Computer Science, EPTCS

SP - 49

EP - 55

BT - Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019)

A2 - Lisitsa, Alexei

A2 - Nemytykh, Andrei

PB - Electronic Proceedings in Theoretical Computer Science

CY - Genova, Italy

T2 - 7th International Workshop on Verification and Program Transformation, VPT 2019

Y2 - 2 April 2019 through 2 April 2019

ER -

Gariano IO, Servetto M, Potanin A, Arora H. Iteratively Composing Statically Verified Traits. In Lisitsa A, Nemytykh A, editors, Proceedings Seventh International Workshop on Verification and Program Transformation (VPT 2019). Genova, Italy: Electronic Proceedings in Theoretical Computer Science. 2019. p. 49-55. (Electronic Proceedings in Theoretical Computer Science, EPTCS). doi: 10.4204/EPTCS.299.7, 10.4204/EPTCS.299.7

Iteratively Composing Statically Verified Traits

Abstract

Publication series

Conference

Access to Document

Other files and links

Fingerprint

Cite this