13
$\begingroup$

Some languages support design by contract in the language itself.

The absolute bare minimum for this is to define:

  • pre-conditions (expects)
  • post-conditions (ensures) &
  • invariants

These are often added as library primitives rather than as part of the language. Adding them to the language gives us the potential for:

  • checking them at compile time
  • running a separate verifier program to formal prove some parts of our specification.

A language I am aware of that trys to support this is Dafny, which describes itself as a verification-aware programming language

On the functional side there are things such as liquid haskell and Idris

Then there are also fully fledged proof assistants like coq which I'm not sure count as "general purpose" languages due to their high level of specialisation.

C++ has also gone a little way in this direction. The standard recently added:

Plans to add

are in the works. And

  • 'full' concepts including concept maps and axioms

were put on hold.

Concepts and contracts elevate design by contract from something typically added via library functions to part of the language that would in theory allow the compiler to use a solver like Z3.

Example contracts syntax:

int mul(int x, int y)
  [[expects: x > 0]]         // implicit default
  [[expects default: y > 0]]
  [[ensures audit res: res > 0]]{
  return x * y;
}

For concepts see for example https://en.cppreference.com/w/cpp/language/constraints

What strategies are there for supporting formal verification in a programming language and what are their pros and cons?

I asked a related question here: What is needed to move from design by contract to using a more advanced prover?

$\endgroup$
2
  • $\begingroup$ Kotlin has a contracts feature too (although it is in the experimental phase). This allows for stuff like "if I'm passed a null, I return a null", and for the type checker to take note of that $\endgroup$
    – Seggan
    Jun 8, 2023 at 15:45
  • $\begingroup$ I couldn't see the justification for removing the link to the related question so I've re-added it. If you want it removed please explain why. $\endgroup$ Jun 9, 2023 at 11:30

2 Answers 2

14
$\begingroup$

Refinement Types

A refinement type is a type with a predicate attached, and all instances must satisfy the predicate.

In Liquid Haskell they're denoted as { x:T | f(x) }, where the type T is refined by the predicate f. In Flux they're denoted T{x:f(x)}, e.g. i32{v:n <= v}. Though both languages have additional syntax to support more invariants

Examples

Liquid Haskell

  • { n:Int | 0 <= n && n < 10 }: an integer in the range [0, 10)

  • { xs:[String] | isSorted xs }: a list of strings which is guaranteed sorted

  • merge :: (Ord a) => x:[a] -> y:[a] -> { v:[a] | (UnionElts v x y) }: a function which takes 2 lists and returns a list containing all elements from both

Flux

#[flux::sig(fn (n:i32) -> i32{v:0<=v && n<=v})]
pub fn abs(n: i32) -> i32 {
    if 0 <= n {
        n
    } else {
        0 - n
    }
}

Takes an integer n and returns an integer which is both non-negative (0<=v) and greater-than-or-equal-to n (n<=v).

#[flux::trusted]
#[flux::sig(fn(self: &strg RVec<T>[@n], T)
            ensures self: RVec<T>[n+1])]
pub fn push(&mut self, item: T) {
    self.inner.push(item);
}

Takes a vector initially of size n and an element, and after returning, the vector is of size n + 1.

Implementations

Pros

  • Intuitive, at least at the surface-level. Many proofs require constructing proofs-as-data which can be very confusing. Refinement types are simply types with predicates, and the predicates are simply expressions in the base language. It's much easier to write { xs:[String] | isSorted xs } than it is to define an inductive ADT which can only represent sorted lists. However, proving that these predicates hold is less intuitive...

  • Pure superset of the language, you simply add extra annotations. The code can still be processed by the base compiler/interpreter if the annotations are comments (which they usually are)

  • Doesn't require much changes to the type system, you simply add an optional predicate to every type. The refinement type system is not very complicated, at least at the surface-level and before adding extensions to prove stronger properties

Cons

  • Not very strong, generally suited for simple proofs like bounded numbers (e.g. for array indexing)

  • Many implementations add extensions on top of the refinement types to prove stronger properties (see first point)

  • Sometimes the compiler can't type-check the refinements, and you must rewrite the predicates in unintuitive and/or verbose ways, and/or provide unintuitive and/or verbose lemmas. It can be difficult and seem archaic even for programmers familiar with theorem proving, if they're familiar with languages like Coq where the proofs are more straightforward (albeit also verbose)

  • Verbose. You're adding extra annotations to a program, and often you must add a lot of these annotations in order to have enough info to prove useful properties. Not to mention writing extra helper functions and lemmas, and "simplifying" your existing functions (actually making them more verbose), to satisfy the solver. Although unfortunately verbosity is a con in most formal methods...

Consensus

So far it sees that the general consensus is that refinement types are great for proving array bounds, sortedness, and other simple properties. However, they can't prove more advanced properties on their own. Personally, I couldn't find any example of a large project which used refinement types; the largest I could find is in the paper LiquidHaskell: Experience with Refinement Types in the Real World, where the Liquid Haskell developers add liquid types to over 10,000 lines of code in popular libraries on Hackage.

The most popular implementation of refinement types is Liquid Haskell. Flux is an upcoming system which will be presented at PLDI 2023, so you may want to keep an eye on that.

  • types projects

See also

$\endgroup$
5
  • $\begingroup$ It seems to me that concepts in C++ (which are really just sugar over templates) count as refinement types. Would you agree? $\endgroup$ Jun 8, 2023 at 7:55
  • $\begingroup$ Could you give some examples of features required/missing for the stronger proofs you mention? I think that overlaps somewhat with my question here . My guess would be maybe quantification operators like forall and exists. $\endgroup$ Jun 8, 2023 at 7:58
  • $\begingroup$ Reading around my related question proofassistants.stackexchange.com/questions/2225/… - suggests that refinement types alone are insufficient. You might also need, at least optionally, soundness and totality $\endgroup$ Jun 8, 2023 at 19:01
  • $\begingroup$ "The refinement type system is not very complicated" — yeah, no more than Dependent Types... :) Originally Refinement Types in F* were formalized without full-blown Dependent Types, but with 4 sorts of kinds, which not very simple by my standards. Still later they "gave up" and went with "honest" Dependent Types (though using extensional theory). $\endgroup$ Jun 11, 2023 at 9:35
  • $\begingroup$ "I couldn't find any example of a large project which used refinement types" — project-everest.github.io is the most well-known and widely-deployed (Windows, Azure, Chrome) I guess... $\endgroup$ Jun 11, 2023 at 9:42
3
$\begingroup$

Hoare Logic

AKA Axiomatic Semantics, or what you call "Design-by-Contract". It was later refined into the Weakest Precondition Calculus by E. W. Dijkstra.

Relatively recently John Reynolds developed it yet further into Separation Logic opening the door for reasoning about mutable references (or pointers), and then Peter O'Hearn evolved it into Concurrent Separation Logic.

These logics or variations thereof form the basis of vast majority of verification tools and frameworks. Most notably, Frama-C, CompCert, Why3, aforementioned Dafny and so on.

(Bounded) Model-Checking

A Model Checker either finds a model with required properties or proves no such model could ever exist. When the model is a (possible) trace of a program execution, a Model Checker can prove that the program never reaches a bad state or provide a counterexample: exact sequence of steps leading to the bad state.

The most basic definition of a "bad state" is a program crash. It might be refined into an unhandled exception, out-of-bounds access, null pointed dereference and so on. The upside is you don't need to specify anything more beyond the language's semantics to check this property.

With minimal additional cleverness we can check that program never executes assert(false), and this lets us verify more interesting invariants than simply "the program doesn't crash" while staying within the vanilla language as long as most languages have assert statements built-in. With Symbolic Model Checking we can verify more complex asserts than simply assert(false) and in a more precise way.

The major obstacle to complete model checking is loops, because it's hard to tell the number of iterations in advance. Hence the use of Bounded Model Checking, which essentially unrolls the loops a finite number of steps.

Overall Model Checking provides huge benefits almost "for free", thus wide variety of Model Checking based tools for many languages with different scopes and capabilities.

Abstract Interpretation

Abstract Interpretation presents a very general framework not only for verification, but almost any program transformations: one can formulate compilation as a sort of Abstract Interpretation if squints hard enough! 😂

Thus again there are a sizeable variety of Abstract Interpretation based tools checking all kinds of program properties, from Python and JavaScript types to Web applications vulnerabilities. But to check more advanced properties one first have to specify these properties. And for specification we often reuse Hoare-style logic or something similar.

$\endgroup$

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .