based on Slides by Jean-Baptiste Tristan & K. Rustan M. Leino |
datatype Peano =
| Zero
| Succ(Peano)
What does Dafny know when we write this definition?
datatype Peano =
| Zero
| Succ(Peano)
datatype Peano =
| Zero
| Succ(Peano)
datatype Peano =
| Zero
| Succ(Peano)
datatype Peano =
| Zero
| Succ(Peano)
In Dafny, all of these can be expressed formally…
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)
Dafny is a type theory:
bool
You can declare the existence of types and give them definitions
A type can be empty
Types can have type characteristics
00
says the type is nonempty
(0)
implies nonempty (00)
NaturalNumber
stands for a fixed but arbitrary, nonempty type
type NaturalNumber(00)
You can declare the existence of constants
They must have a type
ghost const zero: NaturalNumber
zero
stands for a fixed but arbitrary constant of type NaturalNumber
Since we are stating zero
's existence, we need to know that NaturalNumber
is nonempty
For now, think of the keyword ghost
as telling us that this constant is a mathematical object, not a programming one
A constant with a function type is called a function
A function symbol can be declared by function
ghost function Successor(n: NaturalNumber): NaturalNumber
Functions can have
Functions have a return type
A function with return type bool
is called a predicate
A predicate symbol can be declared by predicate
ghost predicate Less(n: NaturalNumber, m: NaturalNumber)
Note that the “: bool
” is implicit for a predicate
A functional (“executable”) expression of type bool
represents a mathematical formula that can be false
or true
They are sometimes called propositions
Propositions can be named using a lemma
lemma Proposition()
ensures forall m: int, n: int :: m > 0 && n > m ==> m + n > 0
A lemma has a name (here, Proposition
)
The proposition stated by a lemma is given after the ensures
keyword
More generally, a lemma names a family of formulas
In the simplest case, the formula is unique
lemma Prop()
ensures forall x: int :: x % 2 == 0 ==> (x / 2) * 2 == x
The lemma can have type parameters and typed parameters
There is one formula for each possible instantiation of these parameters
lemma Prop<T>(x: T)
ensures x == x
A lemma can have a requires
clause, which is a precondition
It restricts the set of formulas to those whose parameterizations satisfy the precondition
lemma Prop(x: int)
requires x % 2 == 0
ensures (x / 2) * 2 == x
requires
and ensures
clauses contain propositions:
lemma Prop(x1: T1,...)
requires proposition expression
ensures proposition expression
bool
are valid propositions
Type: bool
// Constants
lemma False()
ensures false
lemma True()
ensures true
// Predicates
lemma Conjunction(a: bool, b: bool)
ensures a && b
lemma Disjunction(a: bool, b: bool)
ensures a || b
lemma Implication(a: bool, b: bool)
ensures a ==> b
lemma Explication(a: bool, b: bool)
ensures a <== b
lemma Equivalence(a: bool, b: bool)
ensures a <==> b
lemma Negation(a: bool)
ensures !a
The language of propositions includes quantifiers that are not functional expressions
type T
ghost predicate P(x: T)
lemma PredicateLogicConnectives()
ensures (forall x: T :: P(x)) is bool
ensures (exists x: T :: P(x)) is bool
Note: propositions need not be computable and they cannot always be compiled
You can quantify over predicates and state properties from second order logic
lemma SecondOrder()
ensures forall P: int -> bool :: forall x: int :: P(x) || !P(x)
In fact, you can quantify over any value and Dafny is a higher-order logic
lemma ThirdOrder()
ensures forall P2: (int -> bool) -> bool :: forall P1: int -> bool :: P2(P1) || !P2(P1)
Dafny is impredicative: a predicate can be defined by quantifying over all predicates
lemma Impredicative()
ensures forall x: T :: forall P: T -> bool :: P(x)
Dafny's polymorphism is predicative: type parameters always appear before typed parameters
Note, Dafny performs a syntactic rewrite called type-parameter completion on signatures1
type List<X>
function F<T>(x: T): T {
x
}
function G(): List -> List { // expands to: function G<_T0>(): List<_T0> -> List<_T0>
F<List> // expands to: F<List<_T0>>
}
Dafny is a partial logic: some propositions, while syntactically correct, are rejected
In this example, Dafny rejects this proposition because 1/x
is not defined for x == 0
lemma Partial()
ensures forall x: int :: x * 1/x == x
Note for experts:
Dafny therefore needs to verify whether a proposition is acceptable
To do so, it actually proves that the proposition is defined
In this example, Dafny can prove that x
will not be equal to 0
lemma Partial()
ensures forall x: int :: x != 0 ==> x / x == 1
Conclusion: in Dafny, the language of propositions depends on provability
And vice versa
You can use Hilbert's Epsilon operator to choose a value satisfying some property
predicate P(x: int)
lemma HilbertEpsilon()
requires forall x: int :: P(x)
ensures var x: int :| P(x); true
Dafny is not referentially transparent2
The following proposition is false in Dafny:
lemma NotReferentiallyTransparent()
ensures (var x: int :| true; x) == (var x: int :| true; x)
You can combine a type and a proposition to define a subset type
type T
predicate P(x: T)
type U = x: T | P(x)
witness *
Elements of type U
are elements of type T
that satisfy predicate P
A subset type is empty if the predicate never holds
The witness
clause allows you to provide a witness if you want to guarantee that the type is inhabited
The witness *
clause says that the type may be empty
Example of nonempty subset type with a witness
type T(00)
ghost const k: T
type U = x: T | true
ghost witness k
If type U
is defined as a subset type of T
then U
is a subtype of T
Consider the following types
type T
predicate P1(x: T)
type U = x: T | P1(x) witness *
predicate P2(x: U)
type V = x: U | P2(x) witness *
U
is a subtype of T
U
are those T
inhabitants x
for which P1(x)
holds
V
is a subtype of U
V
are those U
inhabitants x
for which P2(x)
holds
V
are those T
inhabitants x
for which P1(x) && P2(x)
holds
Function type A -> B
is a subtype of C -> D
if
C
is a subtype of A
B
is a subtype of D
lemma Subtyping(h: (V -> T) -> bool, f: U -> U)
ensures h(f)
If a type operator S
is covariant in its parameter (declared with +
) then
U
is a subtype of V
, then S<U>
is a subtype of S<V>
type S<+X>
lemma Subtyping(f: S<U> -> bool, y: S<V>)
ensures f(y)
If a type operator S
is contravariant in its parameter (declared with -
) then
U
is a subtype of V
, then S<V>
is a subtype of S<U>
type S<-X>
lemma Subtyping(f: S<U> -> bool, y: S<T>)
ensures f(y)
To ensure that it remains consistent, Dafny sometimes rejects the definition of a type operator
type S<!X> = X -> bool
In this example, because of how the type parameter X
is used, Dafny asks for the parameter to be marked as !
This limits the how it can be instantiated
A covariant type parameter that needs to be restricted is declared as *
instead of +
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
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
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
}
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
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
}
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
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)
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)
Instead, the function can be defined
ghost function Factorial(n: int): int
requires 0 <= n
{
if n == 0 then 1 else Factorial(n - 1)
}
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)
}
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
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)
But you can just define algebraic datatypes to get the same theory
datatype Peano =
| Zero
| Succ(Peano)