Definitions

Jean-Baptiste Tristan & K. Rustan M. Leino

Axioms

The lemmas we have declared so far are (schemas of) axioms

By declaring the lemma we are making a statement that it is true

  lemma Axiom()
    ensures forall m: int, n: int :: m + n == n + m

Defining mathematical objects

When we axiomatize theories:
- We posit the existence of mathematicals objects such as types, constants, functions, and predicates
- We declare their properties
In general, declaring axioms must be avoided
- It is surprisingly easy to make a mistake leading to an inconsistent theory
Rather than assuming the existence of mathematical objects, it is better to define them

Defining constants

Rather than:

  ghost const x: int

  lemma EssenceOfX()
    ensures x == 0

A constant can be defined by assigning it an expression
```
  ghost const x: int := 0
```

Defining simple functions

Rather than:

  ghost function Increment(n: int): int

  lemma EssenceOfIncrement(n: int)
    ensures Increment(n) == n + 1

A function can be defined by providing it with a body

This body can be a functional expression

  ghost function Increment(n: int): int {
    n + 1
  }

Defining functions with quantifiers

The body of a mathematical function can also be a non-functional expression

  ghost predicate Valid(P: int -> bool) {
    forall x: int :: P(x)
  }

In general, a mathematical function may or may not be computable

Defining partial functions

Rather than:

  ghost function Divide(m: int, n: int): int

  lemma EssenceOfDivide(m: int, n: int)
    requires n != 0
    ensures Divide(m, n) == m / n

You can define a partial function

  ghost function Divide(m: int, n: int): int
    requires n != 0
  {
    m / n
  }

Defining functions by description

Hilbert's epsilon operator can be used to define functions

  predicate P<T>(m: T, n: T)

  ghost predicate Prop<T(!new)>(m: T) {
    exists n: T :: P(m, n)
  }

  ghost function F<T>(m: T): T
    requires Prop(m)
  {
    var n :| P(m, n);
    n
  }

You will rarely need this for routine program verification

Axiomatizing recursive functions

A function can be recursive

  ghost function Factorial(n: int): int

  lemma FactorialProp0()
    ensures Factorial(0) == 1

  lemma FactorialProp1(n: int)
    requires n > 0
    ensures Factorial(n) == n * Factorial(n - 1)

Danger of axiomatizing recursive functions

Axiomatizing recursive functions is error prone

  ghost function Factorial(n: int): int

  lemma FactorialBogus1(n: int)
    ensures Factorial(n) == n * Factorial(n - 1)

  lemma FactorialBogus2(n: int)
    ensures Factorial(n) == n * Factorial(n)

Defining recursive functions

Instead, the function can be defined

  ghost function Factorial(n: int): int 
    requires 0 <= n
  {
    if n == 0 then 1 else Factorial(n - 1)
  }

Existence of recursive functions

This raises an important question: how can Dafny ensure that this function actually exists?
One way is to make sure that the definition of the function is well-founded
Intuitively, it means that the function alwasy terminates
In the same way that Dafny tries to prove that propositions are defined automatically
- It also tries to prove that a function definition is well-founded on its own
- When it cannot, you need to help Dafny

Termination — easy case

In most cases, the termination metric is obvious and Dafny can infer it

  function Sum(n: int): int
    decreases n // this line can be omitted, because Dafny will infer it
  {
    if n <= 0 then 0 else Sum(n - 1)
  }

Termination — harder case

If not, you can give it a termination metric using a decreases clause

  function SumUpTo(counter: int, upTo: int): int
    decreases upTo - counter // here, the decreases clause is needed; Dafny will not infer it
  {
    if upTo <= counter then
      counter
    else
      counter + SumUpTo(counter + 1, upTo)
  }

The decrease clause is an expression that decreases at every recursive call

Defining recursive functions: beyond well-founded ordering

There are functions that exist and that are not well-founded

  predicate Closure<T(!new)>(Relation: (T, T) -> bool, x: T, y: T)

  lemma ClosureProp1<T(!new)>(Relation: (T, T) -> bool, x: T)
    ensures Closure(Relation, x, x)

  lemma ClosureProp2<T(!new)>(Relation: (T, T) -> bool, x: T, y: T)
    ensures exists z: T :: Relation(x, z) && Closure(Relation, z, y)

Least predicates

Such a function can be declared as a least predicate

  least predicate Closure<T(!new)>(Relation: (T, T) -> bool, x: T, y: T) {
    || x == y
    || (exists z: T :: Relation(x, z) && Closure(Relation, z, y))
  }

In this case, Dafny ensures that the function actually exists based on its type and body
You will rarely need this for routine program verification

Definition of theories

When we axiomatize a theory, we posit the existence of types, constants, functions, …

  type Peano(0) 

  ghost const Zero: Peano 

  ghost function Succ(n: Peano): Peano 

  lemma PeanoInjectivity(m: Peano, n: Peano)
    requires Succ(m) == Succ(n)
    ensures m == n

  lemma PeanoDiff(n: Peano)
    ensures Succ(n) != Zero 

  lemma PeanoExhaustive(n: Peano)
    ensures n == Zero || exists m: Peano :: n == Succ(m)

  lemma InductionPrinciple(P: Peano -> bool) 
    requires P(Zero) 
    requires forall n: Peano :: P(n) ==> P(Succ(n))
    ensures forall n: Peano :: P(n)

Definition

Algebraic datatypes are a powerful tool to summarize all this in one definition
```
  datatype Peano = 
    | Zero 
    | Succ(Peano)
```