Contract-LIB
A Common Interchange Format
for Software System Specification
Presentation at the Alpine Verification Meeting 2024, Freiburg im Breisgau
Draft: https://www.sosy-lab.org/people/ernst/
Code: https://github.com/gernst/contract-lib
To appear at SpecifyThis @ ISoLA 2024
Gidon Ernst

Wolfram Pfeifer
Mattias Ulbrich2/17

Build-a-Deductive-Verifier Checklist
💡have a new cool idea✓🍵target programming language✓★

foundational methodology✓∀∃

mathematical specification language✓(think: a tool like Dafny)

3/17

Build-a-Deductive-Verifier Checklist
💡have a new cool idea✓🍵target programming language✓★

foundational methodology✓∀∃

mathematical specification language✓

have fun verifying programs

4/17

Build-a-Deductive-Verifier Checklist
have a new cool idea✓🍵target programming language✓★

foundational methodology✓∀∃

mathematical specification language✓📑

support the standard library... ⌛🔌

share verified code / specs across tools... !?

🔌share proof artifacts across tools... !?

🔌connect proofs across languages... !?

hindering progress
towards “real world”

💡5/17

6/17

Tool Interoperability●On the wish-list since forever●Conflict●[e.g. Rushby 2005]–innovation

yay cool research!

[Separation Logic, ...]

–maturity

yay practical impact!

[De Gouw+ 2015]

Landscape of deductive verifiers–🔒 tool lock-in, reinventing the wheel–⪿ standards are rather complex[JML, ACSL]

key challenge: find simple common groundFirst Attempt: ArrayList in Dafnyclass ArrayList<T> {var data: array<T>
var length: int

method add(last: T)
ensures length == old(length) + 1
ensures data[old(length)] == last
ensures forall i :: 0 <= i < old(length) ==>data[i] == old(data[i])}7/17First Attempt: ArrayList in Dafnyclass ArrayList<T> {var data: array<T>
var length: int

bad abstraction● leak implementation details● leak language semantics● leak verification details

method add(last: T)
ensures length == old(length) + 1
ensures data[old(length)] == last
ensures forall i :: 0 <= i < old(length) ==>data[i] == old(data[i])}8/17Software Verification (Principled Approach) 9/17
implementation

specification

laws ofprogramming

data structurespointers etc, ...

data abstractions(sequences, sets,maps, trees, ...)

Second Attempt: ArrayList in Dafnyclass ArrayList<T> {var data: array<T>
var length: int
ghost var content: seq<T>behavior: easy & intuitive● implementation as well as
abstraction mechanism isprivate to the class●method add(last: T)
ensures

content == old(content) + [last]requires valid()
ensures

valid()

predicate valid() { ... }
}

10/17

11/17

Key Observation
complex & difficult
innovation happens here

👻 well-understood
stable across tools

laws ofprogramming
objects
data structurespointers etc, ...

data abstractions(sequences, sets,maps, trees, ...)

Lesson from SMT-LIB etc...:Have a clear &well-defined scope

12/17
👻 well-understood
stable across tools

laws ofprogramming
objects
data structurespointers etc, ...

data abstractions(sequences, sets,maps, trees, ...)

Contract-LIB: Contribution
●

13/17

identify simple common ground–behaviors of well-encapsulated stateful components / OOP–

be independent of language, method, tool–

but be universally compatible (... maybe not with Rust)

Contract-LIB: Contribution●●14/17

identify simple common ground–behaviors of well-encapsulated stateful components / OOP–

be independent of language, method, tool–

but be universally compatible (... maybe not with Rust)define easy-to-adopt technical realization: SMT-LIB with–old, par, standardize extra theories ( Map, Seq, Set)–

declare-abstractions

data model of abstract state–define-contract

behavioral model for methods

ArrayList Interface in Contract-LIB(declare-abstractions((ArrayList 1))((par (T)((ArrayList(ArrayList.content (Seq T)))))(define-contractArrayList.add(par (T) ((this (inout ArrayList)) (last (in T)))((true(= (ArrayList.content this)(seq.++ (old (ArrayList.content this))(seq.unit last))))))

15/17

Summary & Outlook

16/17

Contract-LIB: define and formalize common ground of specifications
across deductive verification tools●

Ongoing: Tool-chain (Java) + Adoption Guidelines●

Outlook: integrate with tools & gather experience●–share specs / verified components across tools–

develop a common repository of case-studies and standard libraries

Paper: design discussion, examples, semantics, integrationguideline, related work (MoXI, CHC, Boogie, Why3, ...)

❤️Acknowledgement: Thanks to all participants in the intense
discussions at Dagstuhl and Lorentz seminars

17/17

Integration Workflow
Contract-LIB
specification
data types● user-defined
functions● abstractions● contracts

VerCors, KeY, Dafny, Viper, Why3, ...

●Language- & toolspecific program
annotations

multiway
import / export

fully precise
behavioral model● template for coupling& framing invariants●

Language-specific●signaturesof operations