Updates

Classes are over. A brief summary is available here.

Exams will take place on 6/12/2022 and 7/12/2022. Please check your individual repositories for more information.

There will be a time slot for questions on 1/12/2022 from 13:00 - 17:00.

Changelog

• 1/11. Added missing slides and examples.
• 24/11. Added slides and code examples for chapter 11 and course wrap-up.
• 15/11. Added slides and code examples for chapter 10.
• 14/11. Added finalized slides for chapter 9; fixed a few typos.
• 04/11. Added finalized slides and code examples for chapter 8 and material for chapter 9.
• 02/11. Added description of the second project.
• 02/11. Added slides and code examples for chapter 8.
• 28/10. Added finalized slides and code examples for chapter 7.
• 26/10. Added slides and code examples for chapter 7.
• 12/10. Added slides and code examples for chapter 6.
• 10/10. Added slides and code examples with solutions for chapter 4.2 and chapter 5. I also fixed a few errors that made it into the slides. The most significant one affects variants for procedures. Thanks to Emil, Christopher, and Yuchen for asking pointed questions that uncovered these issues!
• 05/10. Added slides and code examples for chapter 4.2 and chapter 5.
• 03/10. Added hint to homework of chapter 4.1
• 30/09. Added slides and code examples with solutions for chapter 4.1
• 28/09. Added slides, code examples, and homework for chapter 4
• 24/09. Fixed broken link to the slides. Thanks Christopher.
• 22/09. Added reading material, homework solutions, and skeletons for the first project.
• 21/09. Added description of the first project. Notice that the updated project deadline is October 27, 23:59. It was chosen such that you do not end up working on multiple projects simultaneously.
• 21/09. Added final slides for chapter 2 with some corrections and comments based on feedback. In particular, equality is now always available as an interpreted symbol. It is not part of the signature anymore.
• 14/09. The slides and code examples for the next class are online now; we will first finish the (updated) material from last lecture. Moreover, fixed a typo in one of the homework tasks (thanks Roberto!).
• 10/09. Added a more detailed description of the reading material on FOL.
• 09/09. The next homework and the material covered in class on 08/09 is now online.
• 07/09. The slides and code examples for the next class are now online.
• 05/09. Corrected dates on this page.
• 03/09. Added more detailed explanations of Floyd-Hoare triples and weakest preconditions, and strongest postconditions, since we were a bit too fast during the lecture.
• 03/09. Corrected a few typos in the formalization. Thanks to Roberto, Oliver, and Oskar for reporting those.
• 01/09. The full material for lecture 1 and the preliminary material for lecture 2 is online.
• 29/08. The course page is online.

General Information

• Course type: MSc, 7.5 ECTS (13 weeks)
• The course spans the period E1B (Fall, see DTU’s academic calendar).
• Classes take place every Thursday, from 13:00 to 17:00.
• Examination: Two projects (in small groups) + oral exams
• Lecturer: Christoph Matheja

This course offers a hands-on introduction to the usage, construction, and theory of automated deductive program verifiers. Students should acquire the skills to apply and extend tool-supported methodologies for developing proven-correct software.

You can read the brief course description below or watch the following (somewhat longer) video in which I will motivate why you might want to learn about program verification, give a quick demo, and outline the topics covered in the course:

What this course is about?

One of the most fundamental questions in computer science is whether the programs we write are correct. In fact, the concern about correctness is as old as computers: Alan Turing already asked in 1949¹

"how can one check a routine in the sense of making sure that it is right?”

Early on, we learn that we should test our programs to increase our confidence in the correctness of our programs. However, as adequately summarized by Turing Award winner Edsgar W. Dijkstra²,

“program testing can be very effective to show the presence of bugs, but it is hopelessly inadequate for showing their absence.”

Dijkstra went on to note that

“the only effective way to raise the confidence level of a program is to give a convincing proof of its correctness.”

This course is concerned with the principles and pragmatics of deductive program verification ­­­­- techniques for deriving such correctness proofs in a machine-checkable, compositional, and automated fashion. All of the highlighted aspects play an important role:

• Deductive reasoning: our proofs must be obtained by drawing only sound conclusions from well-known assumptions.
• Machine-checkable: our proofs must be machine-checkable to rule out human errors and allow for changes to our programs without starting proving their correctness all over (on a piece of paper) again.
• Compositional: to scale to whole software projects, we must derive proofs of large programs from existing proofs of smaller programs. Moreover, changing aspects of one software component should not affect the correctness of other components that do not depend on it.
• Automated: while fully automated verification is, in general, not possible (due to known undecidability results), we want to require as little interaction from programmers as possible. Ideally, programmers should only specify the desirable properties a program.

Examples of verification technology in the wild

• Ada Spark is a programming language for safety-critical application domains, such as software for airplanes, that comes with a verification toolset.
• The highest levels of the Automotive Safety Integrity Level (ASIL D) strongly recommend that formal verification is applied to software implementations.
• Program Verification at Microsoft
• Formal Verification in Amazon's Automated Reasoning Group

What will we do in the course?

The course will cover the technology stack underlying modern deductive verification tools from the bottom up by introducing a verifier for a small core language and then progressively enriching the language with advanced features such as a mutable heap, objects, and concurrency. For each language extension, it will explain the necessary reasoning principles, specification techniques, pragmatics, and tool support. In particular, the course will introduce:

1. program logics for writing formal correctness proofs;
2. SMT solvers for automating reasoning about logical formulas and, thus, program proofs;
3. intermediate verification languages in which we can encode verification methodologies targeting, for example, recursive procedures, loops, termination, mathematical datatypes, mutable heap, object-oriented programs, and concurrency; and
4. source code verifiers for handling feature-rich programming languages.

References

Preliminaries

Course participants are expected to be familiar with basics of mathematical logic and program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.

In particular, throughout the course we will

• read and write formulas in first-order predicate logic,
• formally reason about the satisfiability and validity of such formulas,
• read and write formal definitions (of terms, formulas, expressions, etc.) using recursive (or inductive) definitions and sets of inference rules, and
• prove properties of such formal definitions, particularly using structural induction.

We give a few pointers to standard textbooks for students looking for a refresher of or an introduction to the above topics. Our notation will be close to these books. All of the listed books are available online for DTU students.

First-order Predicate Logic

A thorough introduction to first-order predicate logic is found in chapters II and III of the following standard textbook:

Heinz-Dieter Ebbinghaus, Jörg Flum, Wolfgang Thomas: Mathematical logic (3. ed.). Graduate texts in mathematics, Springer 2021, available online.

The syntax of first-order predicate logic is discussed in chapter II.3. The semantics of the logic via the satisfaction relation $\models$ is covered in chapters III.1 - III.3. Satisfiability and validity of predicate logic formulas is defined in chapter III.4.

Notation

Throughout the course, we will write logical formulas using two notations: the (easier typable) notation used by verification tools and the (more concise, perhaps easier readable) notation commonly known from mathematics (as in the book referenced above).

The table below compares both notations and summarizes the semantics of formulas $F,G,H$ in first-order predicate logic for a structure $\mathfrak{A}$ and an interpretation $\mathfrak{I}$. Here, t, t1, ..., tn are terms, that is, expressions constructed from constants, variables $x$, and function applications (interpreted by the structure $\mathfrak{A}$, e.g. standard arithmetical operations). $\mathfrak{I}(t)$ denotes the valuation of term $t$ using interpretation $\mathfrak{I}$. R denotes a relational symbol (interpreted as the relation $R^{\mathfrak{A}}$ by the structure $\mathfrak{A}$) that takes some finite number n >= 0 of terms as argument. An example is the relational symbol =, which is interpreted as the equality relation between terms by every structure under consideration. For binary relations such as =, we often use infix notation t1 = t2 instead of =(t1, t2).

We also give the semantics of $F$ using the satisfaction (or model) relation $\mathfrak{I}\models F$ (read: interpretation $\mathfrak{I}$ satisfies formula $F$); details are found in the above textbook, chapter III.3. We denote by $\mathfrak{I}[x\text{:=}a]$ the update of interpretation $\mathfrak{I}$ in which we assign value $a$ (taken from the universe of structure $\mathfrak{A}$) to variable $x$.

Furthermore, a formula $F$ is satisfiable if there exists an interpretation $\mathfrak{I}$ such that $\mathfrak{I}\models F$. The formula is called valid if $\mathfrak{I}\models F$ holds for every interpretation $\mathfrak{I}$.

Operational Program Semantics & Structural Induction

We recommend two standard textbooks:

Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer 2007, available online.

Chapter 1 gives an overview, including a brief introduction to structural induction. Chapter 2 discusses operational semantics in a style similar to the one used in the lecture.

Glynn Winskel: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press 1993, available online.

Operational program semantics is covered in chapter 2. Chapters 3 and 4 give a detailed discussion of inductive definitions, inference rules, and proving properties about such definitions using various induction principles.

Tools

Throughout the course, we will use the Viper verification infrastructure and the SMT solver Z3. Installation instructions are found below. Please bring a device on which these tools are installed to each lecture.

Viper

The Viper verification infrastructure comprises a programming language (silver but also often just called Viper) and two verification backends (called silicon and carbon).

To install Viper, first make sure that a 64-bit version (e.g. OpenJDK) of Java 11+ is installed on your machine. This may not be the default installation on your machine (for example when installing through a package manager) or the default version offered as a download. Furthermore, make sure that the JAVA_HOME environment variable points to your Java installation (details).

We will use Viper through the Viper IDE, an extension to the free, open-source editor Microsoft Visual Studio Code (VS Code for short).

To install the Viper IDE proceed as follows:

1. Make sure to have the latest version of VS Code (64-bit) installed.
2. Open VS Code
3. Go to the extension browser (⇧+Ctrl+X or ⇧+⌘+X)
4. Search for Viper (see screenshot below).
5. Install the extension and restart VS Code.
6. Create an empty file test.vpr and open it with VS Code.
7. The Viper extension should now install all required dependencies.
8. If everything works, the Viper IDE should report verification successful for the file test.vpr.

Z3

We will also use the SMT solver Z3, originally developed by Microsoft research.

Precompiled binaries for most operating systems are available here.

Alternatively, you can use the python tool pysmt to install Z3, use the docker image, or compile Z3 yourself.

To test your installation of Z3, run the command line tool create a file test.smt2 with the following content:

(declare-const p Bool)
(assert (and p (not p))) 
(check-sat)

Running z3 test.smt2 should then output unsat.

Note: If you are using Windows and want to use Z3 through one of the existing APIs, for example the python bindings, then you also need to install Visual Studio Code.

Frequently Asked Questions

Table of contents

• Organization
• Examination
• Reading material
• Tools and technical difficulties
• Other Questions

Organization

Q: What are the preliminaries for the course? How should I prepare?

A: We expect all participants to be familiar with first-order predicate logic and the basics of program semantics. The necessary background can, for example, be obtained in the DTU courses 02141 and 02156.

A brief recap of the necessary theoretical background is found on the preliminaries page.

Moreover, we expect fluency in at least one functional or object-oriented programming language.

Q: How are the 4 hour slots of each class structured? Is it going to be a 4-hour lecture or will there first be a lecture and them some exercises or lab work?

A: Exercise sessions are integrated into the lecture. In the lecture slides, exercises sessions have a red background. You will get some time to work on those exercises in class before we discuss solutions and proceed with the lecture.

So there will be neither 4-hours of straight lecturing nor a separation between lectures and exercises.

Q: What should I do before the weekly class on Thursday?

A: There will be homework, published on this webpage, which typically consists of a reading assignment and a few exercises to work on.

Q: Why does the course not cover topic X?

A: Obviously, some choices had to be made to fit the course into the usual 13 week schedule. I would be happy if you let me know why you think that topic X is particularly relevant for program verification (and what should be removed).

Q: What are the learning objectives of the course?

A student who has met the objectives of the course will be able to:

• specify functional correctness properties of imperative programs;
• use automated verification tools to develop formally verified software;
• justify why a program meets its specification based on sound reasoning principles;
• explain the technology stack involved in building automated verification tools;
• compare deductive program verification to other methods aiming at increasing confidence in software correctness;
• encode verification-related decision problems to SMT (satisfiability modulo theories);
• identify potential bottlenecks in existing SMT encodings;
• construct sound methodologies for program verification problems, automate these methodologies via encodings to SMT, and justify the involved design decisions;
• achieve the above goals in a group effort while at the same time maintaining individual accountability; and
• communicate solutions to problems in a clear and precise manner.

Examination

Q: How is this course graded?

A: Your grade is determined by:

1. The completeness and quality of group projects (size: 2-3).
   • 15% Homework: preparation for projects
   • 40% Project A: build a verification tool from scratch
   • 60% Project B: design a new verification methodology
2. An individual oral exam
   • Project presentation (ca. 7min, no slides needed)
   • Discussion of projects and course content (ca. 20 min)

Q: Why do the percentages for the projects and homework submissions add up to 115%?

A: For the final grade, we will assume the total percentage is 100%. The additional 15% can be seen as a potential reward for actively working on the homework tasks.

Q: Are there old exams or other material from previous years that I can check out?

A: No, because this is the first time this course is running at DTU.

Reading material

Q: Is there a book on which the course is based?

A: No. All material required for the course will be made available online via this webpage. We will occasionally provide further references but reading them is optional.

Tools and technical difficulties

Q: Which programming language do we have to use in our projects?

A: That is your choice. You can, however, ask us for recommendations :)

Q: I have problems installing one of the tools used in the course.

A: If you have followed all installation instructions step by step and still encounter issues, please contact the teacher as soon as possible.

Q: While working on one of the assignments or projects, I get strange looking errors from one of the tools. What should I do?

A: First, try to reduce your code to a minimal example that fails. If the problem persists, contact the teaching staff with that minimal example and the error.

Other Questions

You are always welcome to ask questions during the lectures. Furthermore, we have two dedicated slots each week for answering questions about the course content, exercises, and projects; the details will be announced in the lecture.

You can, of course, also contact the teacher.

Introduction & Foundations

Preconditions

Files:     [Slides]     [Code skeletons]

We will work with various tools, including the Viper verification infrastructure. Please bring a device on which you can run Viper (requires Java and VS Code) to the lecture. A guide for installing Viper is found here.

Furthermore, we will expect you to read and write simple formulas in (mostly quantifier-free) predicate logic. Suitable literature to (re-)gain the necessary background is found in the preliminaries. The same page also briefly introduces our notation for these formulas.

Postconditions

Files:     [Slides with solutions]     [Full code examples]

What you should have learned after completing chapter 1:

• Program verification means proving that a program meets its specification.
• How automated program verifcation compares, on a high level, to other techniques that aim to increase our confidence in the correctness of software.
• What is the look and feel of automated verifiers that follow the principle of verification like compilation, including modular reasoning with contracts, incremental construction of verified code, and the notion of a trusted codebase.
• Program verification relies on rigorous mathematical definitions. We formalize the verification problem using Floyd-Hoare triples. There are different notions of validity or correctness for such triples; the strongest one is total correctness.
• To check whether a Floyd-Hoare triple is valid, we attempt to construct a verification condition, a logical predicate, which we can then check for validity, that is, it must be true for all possible program states.
• There are two systematic approaches for constructing verification conditions: start at the precondition and construct a suitable predicate by moving forward through the program or start at the postcondition and move backward through the program. The resulting predicate transformers compute the strongest postcondition and the weakest precondition, respectively.
• How weakest preconditions compare to strongest postconditions.

Homework

Reading assignment

The course page contains additional material that you should be able to read after attending the lecture; it might also help you with the homework tasks. In summary:

• Chapter 4.1 describes the fragment of the Viper language used in the lecture.
• Chapter 4.2 formally defines the syntax and semantics of the PL0 language.
• Chapter 4.3 formally defines Floyd-Hoare triples for the PL0 language.
• Chapter 4.4 formally defines weakest preconditions for the PL0 language.
• Chapter 4.5 formally defines strongest postconditions for the PL0 language.

Most of these pages give more precise definitions than those we used on the lecture slides, but nothing is conceptually new. Go over the above chapters and check for yourself if you can follow the formalization. If something is unclear, add questions to your submission in a file QUESTIONS.md or ask them during question time.

Furthermore, remember to prepare for the next lecture.

Tasks

Submission deadline: Thursday, September 8, 12:59 (right before the lecture).

Please submit your solutions by pushing all relevant files to the GitLab repository assigned to your group. If you have not been assigned a repository yet, contact the teacher.

Task 1 (5 points): Forward reasoning with Viper

For each of the Viper programs below, replace TODO by the strongest predicate such that the contract verifies; try to find a predicate that is as simple as possible.

Hint: Use the Viper verifier to check whether the program verifies for your your proposed predicates.

(a)

method a(x: Int, y: Int) returns (z: Int)
    requires 0 <= x && x <= y && y < 100
    ensures TODO
{
    z := y - x
}

(b)

method b()
{
    var x: Int 
    assume 0 <= x && x < 100 
    x := 2 * x 
    assert TODO
}

(c)

method c() {
    var x: Int 
    var y: Int 

    assume x > 0 && x < y 

    x := x + 23
    y := y - 3 * x 

    assert TODO
}

(d)

method d() {
   var x: Int       
   var y: Bool

   assume x > 0
   
   x := x + 1
   if (y) {
     var z: Int
     x := x + z
   } else {
     x := 42
   }

   assert TODO
}

Task 2 (5 points): Backward reasoning with Viper

For each of the Viper programs below, replace TODO by the weakest predicate such that the contract verifies; try to find a predicate that is as simple as possible.

Hint: Use the Viper verifier to check whether the program verifies for your your proposed predicates.

(a)

method a(x: Int, y: Int) returns (X: Int, Y: Int)
    requires TODO
    ensures X == y && Y == x
{
    X := y - x
    Y := y - X
    X := Y + X
}

(b)

method b() {

    var x: Int 
    var y: Int 

    assume TODO

    x := x + y 
    y := x * y

    assert x > y
}

(c)

method c() {
    var x: Int 
    var y: Int 

    assume TODO

    if (y > 5) {
        y := x - y
    } else {
        x := y - x
    }

    assert x > 7
}

(d)

method d(x: Int) returns (y: Int) 
    requires TODO
    ensures y % 2 == 0
{
    if (x < 17) {
        if (x > 3) {
            y := 1
        } else {
            y := 2
        }
    } else {
        y := 6
    }
}

Task 3 (7 points): Encoding conditionals

The language PL0 is simplistic and does not support basic statements (see full definition), such as conditionals if (b) { S1 } else { S2 }. Such a statement evaluates the Boolean expression b in the current program state; if the result is true, we execute S1; otherwise, we executes S2.

In terms of our formal operational semantics, the semantics of conditionals is given by the following inference rules:

$$\frac{b,\sigma {⟹}_b\text{true}}{\text{if (b) { S1 } else { S2 }},\sigma ⟹S1,\sigma }\frac{b,\sigma {⟹}_b\text{false}}{\text{if (b) { S1 } else { S2 }},\sigma ⟹S2,\sigma }$$

(a) Define the weakest precondition of conditionals, that is, WP(if (b) { S1 } else { S2 }, Q).

(b) Define the strongest postcondition of conditionals, that is, SP(P, if (b) { S1 } else { S2 }).

(c) Encode the conditional if (b) { S1 } else { S2 } as a PL0 program. That is, write a PL0 program ENC(if (b) { S1 } else { S2 }) that models the effect of a conditional.

Hint: You may write ENC(S1) and ENC(S2) do denote statements the S1 and S2 to which the encoding of conditionals has already been applied.

(d) Prove that your encoding in (c) is correct in the sense that it yields verification conditions that are logically equivalent to the direct definitions of WP and SP from (a) and (b). That is, show that

• WP(if (b) { S1 } else { S2 }, Q) <==> WP(ENC(if (b) { S1 } else { S2 }), Q) and
• SP(P, if (b) { S1 } else { S2 }) <==> SP(P, ENC(if (b) { S1 } else { S2 })) are valid, where <==> denotes logical equivalence.

Task 4 (8 points): Forward reasoning about total correctness

In the lecture, we noticed a difference between weakest preconditions and strongest postconditions: for strongest, the computed verification condition is valid even if the program encounters a runtime error. This corresponds to the notion of partial correctness. By contrast, the verification conditions obtained from computing weakest preconditions consider total correctness, that is, they enforce safety (i.e., the absence of runtime errors) and termination.

To enable forward reasoning about total correctness, we need to compute a second verification condition that enforces safety.

(a) Give a recursive definition of a predicate transformer SAFE: Pred --> PL0 --> Pred such that the predicate SAFE(P, S) is the verification condition that needs to be checked to enforce that starting S on any state in precondition P does not lead to a runtime error. As for strongest postconditions, SAFE(P, S) should reason about statements in forward direction.

Hint: It might help to first express the same safety property in terms of weakest preconditions.

(b) Using your definition in (a), prove that, for all PL0 statements S and all predicates P, Q, we have

P ==> WP(S, Q) valid
if and only if
SAFE(P, S) valid and SP(P, S) ==> Q valid

Hint: Proceed by structural induction on the syntax of statements S.

Viper cheat sheet

This page briefly summarizes the Viper features that we have seen in the first lecture. If you have not installed Viper yet, please first follow the installation steps.

Further details about Viper are found in the official Viper tutorial. However, do not expect to understand parts about features that we have not covered yet in the course.

Viper programs are stored in .vpr files. They can be verified with two backends: silicon and carbon. silicon is the default and carbon is close to the approach that we will follow throughout the lecture. Ideally, your programs should always verify with both backends. However, for complex examples, one backend might be significantly slower than the other.

Methods

Most Viper code must be placed in methods of the form

method <name>(<inputs>) 
    returns <outputs>
    requires <precondition>
    ensures <postcondition>
{
    <statements>
}

Here, <name> is a name that is unique for the whole Viper program.

<inputs> is a comma-separated list of variable names and their types (so far: Int or Bool). For example, a list of inputs could be x: Int, y: Bool, z: Bool. All input variables are read-only.

Analogously, <outputs> is a comma-separated list of variable names and their types of outputs. Outputs are read-write, but initially have an unknown value. Viper does not have a return statement. The last value assigned to each output variable is returned implicitly when the method terminates.

The variable names used in inputs and outputs are not allowed to overlap.

A method can have zero or more preconditions (predicates such as x > 0 && x < n) indicated by requires. Preconditions may contain input variables but no output variables.

A method can have zero or more postconditions (predicates such as x > 0 && x < n) indicated by ensures. Preconditions may contain both input and output variables.

A method is called abstract if it has no implementation { <statements> }.

Statements

Implementations of Viper methods consist of:

• local variable declarations var <name>:<type>, for example var x: Int; all variable names within a Viper method (including input and output parameters) must be unique;
• assignments <var> := <expression>, where <var> is either an output variable or a previously declared local variable and <expression> is a standard arithmetic expression;
• assertions assert <predicate>, for example assert x > 0, which causes an error if we can reach the assertion in a state that does not satisfy the predicate (otherwise nothing happens);
• assumptions assume <predicate>, which let the program proceed only with states in which the predicate holds;
• standard conditionals if (<boolean expression>) { <statement> } else { <statement> }; and
• standard sequential composition ; between statements; for statements in different lines, the semicolon can be omitted.

Example

For example, the three methods below cover all Viper features that we have encountered in the first lecture. The comments (//) indicate the role of each line.

// every method must have a unique name
method first(x: Int, y: Int, z: Bool) // method three read-only input parameters
    returns (a: Int, b: Bool) // uninitialized output parameters
    requires x < y // precondition, can only refer to input parameters
    requires y > 0 // another precondition
    requires z == true // another precondition
    ensures !b // postcondition, can refer to input and output parameters
    ensures a == x + 2 * y // another precondition
{ // begin of method body
    var u: Int // declaration of local integer variable
               // every variable name can appear at most once in every method
    u := x + y // assignment to local variable
    a := u + y // assignment to output variable
               // the final value of each output is returned
    if (z) { // conditional
        b := false // assignment to output variable of type Bool
    } else {
        b := true
    }
} // end of method body

// An abstract method is a method without a body.
// Such methods are trusted and their verification never fails.
// By default, the input parameters are empty.
// By default, pre- and postconditions are true.
method second() returns (x: Int) 
    ensures x > 0

// the "returns" can be omitted if a method has no outputs
method third()
{
    var a: Int 
    a := second() // a method call that assigns the output to a
    assert a > 0 // assertion; verification fails if we cannot guarantee the condition

    var b: Int 
    assume b > 2 // an assumption; from now on, the verifier proceeds as if b > 2
    var c: Bool

    // all method outputs need to be assigned during a call
    // here, the first output is assigned to b and the second to c.
    b, c := first(2, b, true)

}

The PL0 language

This page formally defines the language PL0 considered in the lecture. It is similar to the Viper language, but not identical.

In particular, the formalization includes

1. variables and constants,
2. the syntax of PL0 programs,
3. our notion of program states and program configurations,
4. the formal semnatics of PL0, including the semantics of arithmetic expressions, Boolean expressions, predicates, and statements.

Variables & Constants

We denote by Var the set of (program) variables, such as x, y, z, etc. Moreover, we typically denote integer-valued constants (of type Int) by c, u, v, w, etc. Analogously, we denote truth values (of type Bool) by t.

Syntax

The syntax of PL0 is composed of

• arithmetic expressions,
• Boolean expressions,
• predicates, and
• program statements.

Arithmetic Expressions

The set AExpr of arithmetic expressions is given by the grammar:

a    ::=    c           (integer-valued constants)
         |  x           (variables)
         |  a + a       (addition)
         |  a * a       (multiplication)
         |  a - a       (subtraction)
         |  a / a       (integer division)
         |  a % a       (remainder)

Boolean Expressions

The set BExpr of Boolean expressions is given by the grammar:

b    ::=    true        (truth)
         |  false       (falsety)
         |  a == a      (equality between arithmetic expressions)
         |  a != a      (inequality between arithmetic expressions)
         |  a <= a      (less-or-equal for arithmetic expressions)
         |  a >= a      (greater-or-equal for arithmetic expressions)
         |  a < a       (less-than for arithmetic expressions)
         |  a > a       (greater-than for arithmetic expressions)
         |  !b          (negation)
         |  b && b      (conjunction)
         |  b || b      (disjunction)

Predicates

The set Pred of predicates P is given by the following grammar:

P    ::=    b                   (Boolean expressions)
         |  exists x :: P       (existential quantification)
         |  forall x :: P       (universal quantification)
         |  !P                  (negation)
         |  P && P              (conjunction)
         |  P || P              (disjunction)
         |  P ==> P             (implication)

PL0 Statements

The set Stmtof program statements S written in PL0 is given by the following grammar:

S    ::=    var x       (local variable declaration)
         |  x := a      (assignment)
         |  assert P    (assertion)
         |  assume P    (assumption)
         |  S;S         (sequential composition)
         |  S [] S      (nondeterministic choice)

Program States

The set States of program states consists of all mappings from finitely many variables to (integer) values, that is,

$$\text{States ::= }\{\sigma :\text{V}\to \text{Int}|\text{V}\subseteq \text{Var},\text{Var}\text{finite}\}.$$

We denote by $\sigma [\text{x}:=\text{v}]$ the state is equal to $\sigma$ except that we assign value $v$ to variable $\text{x}$, that is, $$\begin{array}{rlr}\sigma [\text{x}:=\text{v}](\text{y})::=& \text{v}& \text{ if }\text{x}=\text{y},\\ \sigma [\text{x}:=\text{v}](\text{y})::=& \sigma (\text{y})& \text{ if }\text{x}\ne \text{y}.\end{array}$$

Notice that the domain of a state $\sigma$, $\text{dom}(\sigma )=\text{V}$, can be enlarged through the update $\sigma [\text{x}:=\text{v}]$, that is, $\text{dom}(\sigma [\text{x}:=\text{v}])=\text{dom}(\sigma )\cup \{x\}$.

Operational Semantics

We will define the semantics of statements using four execution relations:

1. a relation ${⟹}_a$ for evaluating arithmetic expressions in a program state;
2. a relation ${⟹}_b$ for evaluating Boolean expressions in a program state;
3. a relation ${⟹}_P$ for evaluating predicates in a program state; and
4. a relation $⟹$ for performing one execution step from one program configuration (a statement coupled with a program state) to another configuration.

Evaluation of arithmetic expressions

For arithmetic expressions a in AExpr, we denote by $\text{a},\sigma {⟹}_a\text{v}$ that evaluating expression a in state $\sigma$ yields integer value v.

Formally, the evaluation relation $${⟹}_a\subseteq (\text{AExpr}\times \text{States})\times \text{Int}$$ is given by the following inference rules:

$$\frac{}{\text{v},\sigma {⟹}_a\text{v}}\frac{}{\text{x},\sigma {⟹}_a\sigma (\text{x})}$$

$$\frac{\bullet \in \{+,-,\ast ,/,\%\}\text{a1},\sigma {⟹}_a\text{v1}\text{a2},\sigma {⟹}_a\text{v2}\text{v}=\text{v1}\bullet \text{v2}}{\text{a1}\bullet \text{a2},\sigma {⟹}_a\text{v}}$$

Notice that the last rule from above uses the standard arithmetic operators on integers v1 and v2 with one exception: we assume that all arithmetic operators are defined for every input, that is, they are total functions. If an operation is not well-defined, then it returns some value but we do not know which one. For example, evaluating 5 / 0 yields such an unknown value. We will address how to spot and report such runtime errors later in the course.

Evaluation of Boolean expressions

For Boolean expressions b in BExpr, we denote by $\text{b},\sigma {⟹}_b\text{t}$ that evaluating expression b in state $\sigma$ yields truth value t.

Formally, the evaluation relation $${⟹}_b\subseteq (\text{BExpr}\times \text{States})\times \text{Bool}$$ is defined by structural induction using the following inference rules:

$$\frac{}{\text{true},\sigma {⟹}_b\text{true}}\frac{}{\text{false},\sigma {⟹}_b\text{false}}$$

$$\frac{\text{a1},\sigma {⟹}_a\text{v1}\text{a2},\sigma {⟹}_a\text{v2}\text{t}=(\text{v1}\bowtie \text{v2})\bowtie \in \{\text{==},\text{!=},\text{<=},\text{>=},\text{<},\text{>}\}}{\text{a1}\bowtie \text{a2},\sigma {⟹}_b\text{t}}$$

$$\frac{\text{b},\sigma {⟹}_b\text{false}}{\text{!b},\sigma {⟹}_b\text{true}}\frac{\text{b},\sigma {⟹}_b\text{false}}{\text{!b},\sigma {⟹}_b\text{true}}$$

$$\frac{\text{b1},\sigma {⟹}_b\text{false}}{\text{b1 \&\& b2},\sigma {⟹}_b\text{false}}\frac{\text{b2},\sigma {⟹}_b\text{false}}{\text{b1 \&\& b2},\sigma {⟹}_b\text{false}}\frac{\text{b1},\sigma {⟹}_b\text{true}\text{b2},\sigma {⟹}_b\text{true}}{\text{b1 \&\& b2},\sigma {⟹}_b\text{true}}$$

$$\frac{\text{b1},\sigma {⟹}_b\text{true}}{\text{b1 || b2},\sigma {⟹}_b\text{true}}\frac{\text{b2},\sigma {⟹}_b\text{true}}{\text{b1 || b2},\sigma {⟹}_b\text{true}}\frac{\text{b1},\sigma {⟹}_b\text{false}\text{b2},\sigma {⟹}_b\text{false}}{\text{b1 || b2},\sigma {⟹}_b\text{false}}$$

In the above rules, we write $\text{v1}\bowtie \text{v2}$ to denote the value obtained from performing a standard comparison $\bowtie$ between two integer values.

Evaluation of predicates

For predicates P in Pred, we denote by $\text{P},\sigma {⟹}_b\text{t}$ that evaluating predicate P in state $\sigma$ yields truth value t.

Formally, the evaluation relation $${⟹}_P\subseteq (\text{Pred}\times \text{States})\times \text{Bool}$$ is defined by structural induction using the following inference rules:

$$\frac{\text{b},\sigma {⟹}_b\text{t}}{\text{b},\sigma {⟹}_P\text{t}}\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{!P},\sigma {⟹}_P\text{true}}\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{!P},\sigma {⟹}_P\text{true}}$$

$$\frac{\text{v}\in \text{Int}\text{P},\sigma [\text{x := v}]{⟹}_P\text{true}}{\text{exists x :: P},\sigma {⟹}_P\text{true}}$$

$$\frac{\dots \text{P},\sigma [\text{x := -1}]{⟹}_P\text{false}\text{P},\sigma [\text{x := 0}]{⟹}_P\text{false}\text{P},\sigma [\text{x := 1}]{⟹}_P\text{false}\dots }{\text{exists x :: P},\sigma {⟹}_P\text{false}}$$

$$\frac{\text{v}\in \text{Int}\text{P},\sigma [\text{x := v}]{⟹}_P\text{false}}{\text{forall x :: P},\sigma {⟹}_P\text{false}}$$

$$\frac{\dots \text{P},\sigma [\text{x := -1}]{⟹}_P\text{true}\text{P},\sigma [\text{x := 0}]{⟹}_P\text{true}\text{P},\sigma [\text{x := 1}]{⟹}_P\text{true}\dots }{\text{forall x :: P},\sigma {⟹}_P\text{true}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{false}}{\text{P1 \&\& P2},\sigma {⟹}_P\text{false}}\frac{\text{P2},\sigma {⟹}_P\text{false}}{\text{P1 \&\& P2},\sigma {⟹}_P\text{false}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{true}\text{P2},\sigma {⟹}_P\text{true}}{\text{P1 \&\& P2},\sigma {⟹}_P\text{true}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{true}}{\text{P1 || P2},\sigma {⟹}_P\text{true}}\frac{\text{P2},\sigma {⟹}_P\text{true}}{\text{P1 || P2},\sigma {⟹}_P\text{true}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{false}\text{P2},\sigma {⟹}_P\text{false}}{\text{P1 || P2},\sigma {⟹}_P\text{false}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{true}\text{P2},\sigma {⟹}_P\text{true}}{\text{P1 ==> P2},\sigma {⟹}_P\text{true}}\frac{\text{P1},\sigma {⟹}_P\text{true}\text{P2},\sigma {⟹}_P\text{false}}{\text{P1 ==> P2},\sigma {⟹}_P\text{false}}$$

$$\frac{\text{P1},\sigma {⟹}_P\text{false}}{\text{P1 ==> P2},\sigma {⟹}_P\text{true}}$$

Program Configurations

A program configuration is either a pair $(\text{S},\sigma )$ consisting of a statement $\text{S}$ and a program state $\sigma$, or a pair $(\text{done},\sigma )$ indicating termination with final state $\sigma$, or $\text{error}$, which indicates the occurrence of a runtime error, or $\text{magic}$ indicating that we ended up in a magical place where anything is possible (i.e., we can verify any property, even wrong ones). Formally, the set $\text{Conf}$ of program configurations is given by

$$\text{Conf ::= }(\text{Stmt}\times \text{States})\cup (\{\text{done}\}\times \text{States})\cup \{\text{error},\text{magic}\}.$$

Execution relation for statements

For PL0 statements S in Stmt, we denote by $\text{S},\sigma ⟹C$ that executing one step starting in configuration $(\text{S},\sigma )$ results in configuration $C$. Formally, the execution relation $$⟹\subseteq \text{Conf}\times \text{Conf}$$ is defined by structural induction using the following inference rules:

$$\frac{\text{v}\in \text{Int}}{\text{var x},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$

$$\frac{\text{a},\sigma {⟹}_a\text{v}}{\text{x := a},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$

$$\frac{\text{P},\sigma {⟹}_P\text{true}}{\text{assert P},\sigma ⟹\text{done},\sigma }\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{assert P},\sigma ⟹\text{error}}$$

$$\frac{\text{P},\sigma {⟹}_P\text{true}}{\text{assume P},\sigma ⟹\text{done},\sigma }\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{assume P},\sigma ⟹\text{magic}}$$

$$\frac{\text{S1},\sigma ⟹{\text{S1}}^{\prime },{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹{\text{S1}}^{\prime }\text{;S2},{\sigma }^{\prime }}\frac{\text{S1},\sigma ⟹\text{done},{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹\text{S2},{\sigma }^{\prime }}$$

$$\frac{\text{S1},\sigma ⟹\text{error}}{\text{S1;S2},\sigma ⟹\text{error}}\frac{\text{S1},\sigma ⟹\text{magic}}{\text{S1;S2},\sigma ⟹\text{magic}}$$

$$\frac{}{\text{S1 [] S2},\sigma ⟹\text{S1},\sigma }\frac{}{\text{S1 [] S2},\sigma ⟹\text{S2},\sigma }$$

Notice that we can always perform at least one step of the execution relation until we reach a final configuration of the form error, magic, or (done, _).

Floyd-Hoare triples

Extended execution relation

Towards a formal definition of Floyd-Hoare triples, we first extend the execution relation $⟹$ to perform exactly $n\ge 0$ (as opposed to exactly one) execution steps:

• $C{⟹}^{0}C$, and
• $C{⟹}^{n+1}{C}^{\prime }$ if $C⟹C^{\prime \prime }$ and $C^{\prime \prime }{⟹}^n{C}^{\prime }$.

We write $C{⟹}^{\ast }{C}^{\prime }$ if there exists some $n\ge 0$ such that $C{⟹}^n{C}^{\prime }$. Furthermore, we write $C{/⟹}^n$ if there exists no configuration $C^{\prime }$ such that $C{⟹}^n{C}^{\prime }$.

Formal Definition

A Floyd-Hoare triple $\{\text{P}\}\text{S}\{\text{Q}\}$ consists of a precondition $\text{P}$ in Pred, a program statement $\text{S}$, and a postcondition $\text{Q}$ in Pred.

Intuitively, a triple is valid if every execution of program $\text{S}$ that starts in a state satisfying the precondition $\text{P}$ will not cause a runtime error (for example, by failing an assertion) and will eventually terminate in a state satisfying the postcondition $\text{Q}$.

Towards a formal definition, recall from the definition of our language that $\text{dom}(\sigma )$ denotes the variables for which the state $\sigma$ is defined. Moreover, let $\text{Var}(\text{P})$ denote all free variables that appear in predicate $\text{P}$. Then $\text{Var}(\text{P})\subseteq \text{dom}(\sigma )$ means that state $\sigma$ assigns values at least to all variables in predicate $\text{P}$.

The Floyd-Hoare triple $\{\text{P}\}\text{S}\{\text{Q}\}$ is valid (for total correctness) if and only if for every state $\sigma$ with $\text{Var}(\text{P})\subseteq \text{dom}(\sigma )$, if $\text{P},\sigma {⟹}_P\text{true}$, then

1. (safety) there exists no $n\ge 0$ such that $\text{S},\sigma {⟹}^n\text{error}$;
2. (termination) there exists $n\ge 0$ such that for every $m\ge n$, $\text{S},\sigma {/⟹}^m$; and
3. (partial correctness) if $\text{S},\sigma {⟹}^{\ast }(\text{done},{\sigma }^{\prime })$ and $\text{Var}(\text{Q})\subseteq \text{dom}({\sigma }^{\prime })$, then $\text{Q},{\sigma }^{\prime }{⟹}_P\text{true}$.

Here, the first condition (safety) ensures that we cannot encounter a runtime error (for example an assertion failure) when starting execution in a state that satisfies the precondition. The second condition ensures termination, that is, we cannot perform execution steps ad infinitum. The third condition makes sure that we satisfy the postcondition whenever we manage to terminate without a runtime error.

We say that a triple is valid for partial correctness, whenever the third (but not necessarily the first or second) property holds.

In principle, we can directly apply the above definition of validity together with our operational semantics to check whether a triple is valid. However, in most cases this is not feasible, since we would have to consider all possible program executions.

Instead, we use verification conditions to reason about the validity of a triple in a symbolic way, that is by reasoning about predicates, without invoking the operational program semantics. In the lecture, we considered two such approaches for constructing verification conditions: weakest preconditions and strongest postconditions.

Weakest preconditions

Weakest preconditions generate a verification condition for checking the validity of Floyd-Hoare triples by starting at the postcondition and moving backward through the program.

Definition

The weakest precondition of a program statement Sand a postcondition Q is the predicate WP describing the largest possible set of states such that the Floyd-Hoare triple

{ WP } S { Q }

is valid for total correctness. In other words, whenever { P } S { Q } is valid, then P implies WP.

Intuition

The weakest precondition is a predicate, which describes all possible initial states (think: inputs) on which we can run program $\text{S}$ such that it terminates without runtime errors in final states (think: outputs) specified by the postcondition $\text{Q}$.

When determining the weakest precondition of a program $\text{S}$ and a postcondition $\text{Q}$, we thus aim to modify $\text{Q}$ in a way that reverts changes made to the state by $\text{S}$. The result is a predicate that is true for a given initial state whenever running $\text{S}$ on that initial state leads to a final state satisfying $\text{Q}$ again. Thus, one can think about the weakest precondition as the predicate that anticipates the truth value of postcondition $\text{Q}$ but before (that is, evaluated in initial states) rather than after (that is, evaluated in final states) running program $\text{S}$.

Computation

We typically do not need to apply the above (semantic) definition, since we can compute weakest preconditions (syntactically) on the program structure using the following recursive definition:

S                       WP(S, Q)
===============================================
var x                   forall x :: Q
assert R                R && Q
assume R                R ==> Q
x := a                  Q[x / a]
S1; S2                  WP(S1, WP(S2, Q))
S1 [] S2                WP(S1, Q) && WP(S2, Q)

Here, Q[x / a] is the predicate Q in which every (free) appearance of x has been replaced by a. A formal definition is given below.

We briefly go over the above rules for computing weakest preconditions.

Variable declarations

The variable declaration var x declares x as an unitialized (integer-valued) variable named x. All information about the value of some other variables named x that might have existed before are forgotten. This is reflected by the operational rule

$$\frac{\text{v}\in \text{Int}}{\text{var x},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$ which nondeterministically assigns any integer $\text{v}$ to x.

Now, assume that postcondition Q holds for the final state $\sigma [\text{x := v}]$. What are the possible initial states such that executing var x could lead to such a state?

In fact, such states must coincide with $\sigma [\text{x := v}]$ for all variables except x, since var x does not change any other variable. Moreover, the value of x does not matter at all, since x will be set to an arbitrary integer by executing var x.

Hence, we can (but, due to nondeterminism do not have to) reach $\sigma [\text{x := v}]$ from any state $\sigma [\text{x := u}]$ for all initial values $\text{u}$ of x.

As a predicate, we can use a universal quantifier over x to express that the value of x does not matter. This yields WP(var x, Q) ::= forall x :: Q.

Assignments

The assignment x := a evaluates expression a in the current (initial) program state and assigns the resulting value to variable x. This is reflected by the operational rule

$$\frac{\text{a},\sigma {⟹}_a\text{v}}{\text{x := a},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$

Similarly to the variable declaration, only variable x is potentially changed by the assignment. However, the original value of x now does matter, since we may need it to evaluate expression a. For example, the assignment x := x + 1 depends on the value of x in the initial state.

Now, assume that postcondition Q holds for the final state $\sigma [\text{x := v}]$. What are the possible initial states such that executing x := a leads to such a state?

Intuitively, we would like to undo the change made by the assignment. For example, if x >= 17 holds after the assignment x := x + 1, then x >= 16 should hold before the assignment. One way to do this is to observe that the expression x + 1 is evaluated in initial states, just like the weakest precondition. We can thus use it to refer to the value v. To undo the assignment, we then replace every occurrence of x by x+1 and obtain x + 1 >= 17.

The effect of such a replacement is that the effect of setting x to the value of x+1 now appears on both sides of every constraint involving x. For the arithmetic operations in our language, they will thus cancel each other out. More concretely, x + 1 >= 17 is equivalent to x >= 16, our desired precondition.

Formally, the weakest precondition of assignments is defined as WP(x:=a, Q) ::= Q[x/a], that is we formally substitute x by a in Q.

The following lemma justifies the above intuition, that is, we can substitute x by a to "undo" the effect of executing the assignment x := a:

Substitution Lemma Consider a predicate $\text{Q}$, an arithmetic expression $\text{a}$, and a state $\sigma$. Moreover, assume that $\text{a}$ evaluates to value $\text{v}$ for state $\sigma$, that is, $\text{a},\sigma \to \text{v}$.

Then, $\sigma [\text{x := v}]\models Q$ if and only if $\sigma \models Q[\text{x / a}]$.

The proof is by structural induction on the syntax of arithmetic expressions and left as an exercise.

Assertions

The assertion assert R checks whether the predicate R holds in the current (initial) state and causes a runtime error if this is not the case; otherwise, it has no effect. This is reflected by two operational rules, one for the case that R holds and one for the case that it does not hold:

$$\frac{\text{P},\sigma {⟹}_P\text{true}}{\text{assert P},\sigma ⟹\text{done},\sigma }\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{assert P},\sigma ⟹\text{error}}$$

Now, assume that postcondition Q holds for the final state $\sigma$. We do not consider the configuration error because reason about total correctness; a triple is not valid if we can reach error from an initial state that satisfies the precondition.

What are the possible initial states such that executing assert R leads to $\sigma$? We first observe that the assertion does not change $\sigma$: if Q holds after execution of assert R, then it also holds before its execution. We then reach the final state $\sigma$ if and only if initial state $\sigma$ additionally satisfies the predicate R.

Hence, the weakest precondition of assertions is defined as WP(assert R, Q) ::= R && Q.

Assumptions

The assumption assume R is a somewhat strange statement because we cannot execute it on an actual machine; it is a verification-specific statement, similar to making an assumption in a mathematical proof. Intuitively, assume R checks whether the predicate R holds in the current (initial) state. Similar to an assertion, there is no effect if the predicate holds. However, in contrast to an assertion, we reach a "magical state" in which everything goes if the predicate does not hold. This corresponds to the case that we have made a wrong assumption in a proof: from a wrong assumption we can conclude whatever we want, so the result becomes worthless. This is reflected by two operational rules, one for the case that R holds and one for the case that it does not hold:

$$\frac{\text{P},\sigma {⟹}_P\text{true}}{\text{assume P},\sigma ⟹\text{done},\sigma }\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{assume P},\sigma ⟹\text{magic}}$$

Now, assume that postcondition Q holds for the final state $\sigma$. As for assertions, we do not consider the configuration magic; executions that move to magic cannot invalidate a triple anyway.

What are the possible initial states such that executing assume R leads to $\sigma$? We first observe that the assertion does not change $\sigma$: if Q holds after execution of assume R, then it also holds before its execution. There are now two cases:

1. $\sigma$ satisfies R and postcondition Q, or
2. $\sigma$ does not satisfy R and we thus do not care about the result due to a wrong assumption; the weakest precondition should be true in this case, since everything follows from a wrong assumption.

Formally, this can be expressed as the predicate (R && Q) || !R or, equivalently, WP(assume R) ::= R ==> Q.

Sequential composition

The sequential composition S1;S2 first executes program S1 and then program S2. This is reflected by four operational rules

$$\frac{\text{S1},\sigma ⟹{\text{S1}}^{\prime },{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹{\text{S1}}^{\prime }\text{;S2},{\sigma }^{\prime }}\frac{\text{S1},\sigma ⟹\text{done},{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹\text{S2},{\sigma }^{\prime }}$$

$$\frac{\text{S1},\sigma ⟹\text{error}}{\text{S1;S2},\sigma ⟹\text{error}}\frac{\text{S1},\sigma ⟹\text{magic}}{\text{S1;S2},\sigma ⟹\text{magic}}$$

Here, the first rule keeps executing S1; termination of S1 is handled by the second rule, which moves on with executing S2. The last two rules propagate the case that we already encountered a runtime error or a wrong assumption.

What are the possible initial states such that executing S1;S2 leads to final states that satisfy postcondition Q?

By the inductive definition of weakest preconditions, we can assume that we already know how to construct weakest preconditions for S1 and S2, namely WP(S2, Q) and WP(S1, WP(S2, Q)). The set of all initial states on which we can run S2 to end up in a state that satisfies Q is given by WP(S2, Q). We can use this predicate as the postcondition of program S1. By the same argument, WP(S1, WP(S2, Q)) is the set of all initial states on which we can run S1 to end up in a state that satisfies WP(S2, Q).

Putting both arguments together, WP(S1, WP(S2, Q)) is the set of all initial states such that running S1 followed by S2 leads us to states that satisfy Q. Hence, the weakest precondition of sequential composition is defined as WP(S1;S2, Q) ::= WP(S1, WP(S2, Q)).

Nondeterministic choice

The nondeterministic choice S1 [] S2 executes either program S1 or program S2; we do not know which one. This is reflected by two operational rules, one for running S1 and one for running S2:

$$\frac{}{\text{S1 [] S2},\sigma ⟹\text{S1},\sigma }\frac{}{\text{S1 [] S2},\sigma ⟹\text{S2},\sigma }$$

What are the possible initial states such that executing S1 [] S2 leads to final states that satisfy postcondition Q? By the inductive definition of weakest preconditions, we can assume that we already know how to construct weakest preconditions for S1 and S2, namely WP(S1, Q) and WP(S2, Q). Since we do not know whether S1 or S2 is executed, we can only guarantee that we will certainly reach a state that satisfies Q if we start in a state from which it does not matter whether we run S1 or S2. Our desired initial states must thus satisfy both WP(S1, Q) and WP(S2, Q).

Hence, the weakest precondition of nondeterministic choice is defined as WP(S1 [] S2, Q) ::= WP(S1, Q) && WP(S2, Q).

Variable substitution

F[x/a] denotes the substitution of every (free) occurence of variable x by expression a in F. It is defined recursively as follows:

F                      F[x/a]
============================================
true                    true
false                   false
x                       a
y                       y    (where x != y)
v                       v
a1 <> a2                a1[x/a] <> a2[x/a]    
                            for <> in { ==, !=, <=, >=, <, >, +, *, - /, % }
Q1 && Q2                Q1[x/a] && Q2[x/a]
Q2 || Q2                Q1[x/a] || Q2[x/a]
!Q1                     !(Q1[x/a])
Q1 ==> Q2               Q1[x/a] ==> Q2[x/a]
exists y :: Q1          exists y :: Q1[x/a]
forall y :: Q1          forall y :: Q1[x/a]

Strongest postconditions

Strongest postconditions generate a verification condition for checking the validity of Floyd-Hoare triples by starting at the precondition and moving forward through the program, just like an ordinary program execution.

Definition

The strongest postcondition of a program statement Sand a pprecondition P is the predicate SP describing the smallest possible set of states such that the Floyd-Hoare triple

{ P } S { SP }

is valid for partial correctness. In other words, whenever { P } S { Q } is valid for partial correctness, then SP implies Q.

Notice that strongest postcondition on their own only make sense for partial correctness. For example, how should we choose SP such that { true } assert false { SP } is valid? There is no SP such that the triple is valid for total correctness. For partial correctness, we have SP = false and, in fact, every postcondition leads to a triple that is valid for partial correctness.

Intuition

The strongest postcondition of a program S and a precondition P is the predicate that consists of all final states in which program S terminates when started on states that satisfy P. It thus corresponds to symbolically executing the program, that is, we run the program by modifying sets of states - described by predicates - instead of single states.

When determining strongest postconditions, we thus aim to modify the precondition such that it captures the changes made to the program states by the executed program.

Computation

Similar to weakest preconditions, we can compute strongest postconditions on the program structure using the following recursive definition:

S                       SP(P, S)
==================================================================
var x                   exists x :: P
assert R                P && R
assume R                P && R
x := a                  exists x0 :: P[x / x0] && x == a[x / x0]
S1; S2                  SP(SP(P, S1), S2)
S1 [] S2                SP(P, S1) || SP(P, S2)

Here, P[x / x0] is the predicate P in which every (free) appearance of x has been substituted by x0.

As for weakest preconditions, we briefly go over the above rules for computing strongest postconditions.

Variable declarations

The variable declaration var x declares x as an unitialized (integer-valued) variable named x. All information about the value of some other variables named x that might have existed before are forgotten. This is reflected by the operational rule

$$\frac{\text{v}\in \text{Int}}{\text{var x},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$ which nondeterministically assigns any integer $\text{v}$ to x.

Now, assume that precondition P holds for the initial state $\sigma$. What are the final states that we can reach by running var x on $\sigma$? The state $\sigma [\text{x := v}]$ for some (nondeterministically chosen) integer $v$. Hence, the strongest postcondition is sp(P, var x) ::= exists x :: P.

Assignments

The assignment x := a evaluates expression a in the current (initial) program state and assigns the resulting value to variable x. This is reflected by the operational rule

$$\frac{\text{a},\sigma {⟹}_a\text{v}}{\text{x := a},\sigma ⟹\text{done},\sigma [\text{x := v}]}$$

Similarly to the variable declaration, only variable x is potentially changed by the assignment.

Now, assume that precondition P holds for the initial state $\sigma$. What are the possible final states that we can reach by executing x := a on $\sigma$?

A first guess might be to define SP(P, x := a) ::= P && x == a, that is, P should still hold and after the assignment x equals a. However, the following triples are not valid:

• { x == 4 } x := 7 { x == 4 && x == 7 }
• { true } x := x + 1 { true && x == x + 1 }

Hence, the above proposal is not necessarily correct if P or a depend on x. The underlying issue is that both P and a are originally evaluated in initial states but the strongest postconditions talks about final states. The variable x is the only variable that might have a different value before and after executing the assignment.

To define the correct strongest postcondition, we introduce an auxiliary variable, say x0, that represents the original value of x when evaluated in some initial state. The predicate P[x / x0] then means that precondition P was true in some initial state; similarly, a[x/x0] refers to the evaluation of a in the same initial state. Put together, we then use the original proposal but state that P and a were true in some initial state.

Hence, the strongest postcondition of assignments is defined as SP(P, x:=a) ::= exists x0 :: P[x / x0] && x == a[x / x0].

As an example, let consider precondition x == 4 and the assignment x := x + 7:

sp(x == 4, x := x + 7)
= (by definition)
exists x0 :: x0 == 4 && x == x0 + 7
= (simplification)
x == 11

Indeed, x will be 11 after running x := x + 7 on a state where x is initially 4.

Assumptions

The assumption assume R is a somewhat strange statement because we cannot execute it on an actual machine; it is a verification-specific statement, similar to making an assumption in a mathematical proof. Intuitively, assume R checks whether the predicate R holds in the current (initial) state; there is no effect if the predicate holds; we reach a "magical state" in which everything goes if the predicate does not hold. This is reflected by two operational rules, one for the case that R holds and one for the case that it does not hold:

$$\frac{\text{P},\sigma {⟹}_P\text{true}}{\text{assume P},\sigma ⟹\text{done},\sigma }\frac{\text{P},\sigma {⟹}_P\text{false}}{\text{assume P},\sigma ⟹\text{magic}}$$

Now, assume that precondition P holds for the initial state $\sigma$. We do not consider the configuration magic; executions that move to magic cannot invalidate a triple anyway.

What are the possible final states that we can reach by executing assume R on $\sigma$?

Since we do not have to consider executions that move to magic, we know that $\sigma$ satisfies R. Moreover, since the assumption that does not change $\sigma$, P also holds in the final state.

Hence, the strongest postcondition of assumptions is defined as SP(P, assume R) ::= P && R.

Assertions

The assertion assert R checks whether the predicate R holds in the current (initial) state and causes a runtime error if this is not the case; otherwise, it has no effect. Since we reason about partial correctness with strongest postconditions, it does not matter whether we reach an error configuration or a magical configuration.

The strongest postcondition of the assertion assert R thus does not differ from the strongest postcondition of the assumption assume R. That is, SP(P, assert R) ::= P && R.

Sequential composition

The sequential composition S1;S2 first executes program S1 and then program S2. This is reflected by four operational rules

$$\frac{\text{S1},\sigma ⟹{\text{S1}}^{\prime },{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹{\text{S1}}^{\prime }\text{;S2},{\sigma }^{\prime }}\frac{\text{S1},\sigma ⟹\text{done},{\sigma }^{\prime }}{\text{S1;S2},\sigma ⟹\text{S2},{\sigma }^{\prime }}$$

$$\frac{\text{S1},\sigma ⟹\text{error}}{\text{S1;S2},\sigma ⟹\text{error}}\frac{\text{S1},\sigma ⟹\text{magic}}{\text{S1;S2},\sigma ⟹\text{magic}}$$

Here, the first rule keeps executing S1; termination of S1 is handled by the second rule, which moves on with executing S2. The last two rules propagate the case that we already encountered a runtime error or a wrong assumption.

What are the possible final states that we can reach when executing S1;S2 on some initial state that satisfies precondition P?

By the inductive definition of strongest postconditions, we can assume that we already know how to construct strongest postconditions for S1 and S2, namely SP(P, S1) and SP(SP(P, S1), S2).

SP(P, S1) is then the set of all final states we can reach after running S1 on a state satisfying P. We then use this predicate as the precondition of S2. By the same argument, SP(SP(P, S1), S2) is then the set of final states we can reach after running S2 on a state satisfying SP(P, S1).

Putting both arguments together, SP(SP(P, S1), S2) is the set of all final states reached after running S1 followed by S2 on initial states that satisfy P.

Hence, the strongest postcondition of sequential composition is defined as SP(P, S1;S2) ::= SP(SP(P, S1), S2).

Nondeterministic choice

The nondeterministic choice S1 [] S2 executes either program S1 or program S2; we do not know which one. This is reflected by two operational rules, one for running S1 and one for running S2:

$$\frac{}{\text{S1 [] S2},\sigma ⟹\text{S1},\sigma }\frac{}{\text{S1 [] S2},\sigma ⟹\text{S2},\sigma }$$

If we run S1 [] S2 on an initial states that satisfy precondition P, then we end up in the states reached by executing S1 on P or in the states reached by executing S2 on P, respectively.

Hence, the strongest postcondition of nondeterministic choice is defined as SP(P, S1 [] S2) ::= SP(P, S1) || SP(P, S2).

Solutions to Homework Tasks

Task 1 (5 points): Forward reasoning with Viper

For each of the Viper programs below, replace TODO by the strongest predicate such that the contract verifies; try to find a predicate that is as simple as possible.

Hint: Use the Viper verifier to check whether the program verifies for your your proposed predicates.

(a)

method a(x: Int, y: Int) returns (z: Int)
    requires 0 <= x && x <= y && y < 100
    ensures 0 <= x && x <= y && y < 100 && z == y - x
{
    // START HERE
    assert 0 <= x && x <= y && y < 100
    z := y - x
    // We do not need an existential since z is fresh
    assert 0 <= x && x <= y && y < 100 && z == y - x
}

(b)

method b()
{
    assert true 
    var x: Int 
    assert exists x0:Int :: true 
    assert true
    assume 0 <= x && x < 100 
    assert 0 <= x && x < 100
    x := 2 * x 
    assert exists x0:Int :: 0 <= x0 && x0 < 100 && x == 2*x0
    assert 0 <= x && x < 199
}

(c)

method c() {
    assert true 
    var x: Int 
    assert true 
    var y: Int 
    assert true

    assume x > 0 && x < y 

    assert x > 0 && x < y

    x := x + 23

    assert x-23 > 0 && x-23 < y

    y := y - 3 * x 

    //assert exists y0:Int :: x-23 > 0 && x-23 < y0 && y == y0 - 3 *x
    assert x-23 > 0 && x-23 <  y + 3*x
}

(d)

method d() {
   assert true
   var x: Int 
   assert true      
   var y: Bool
   assert true

   assume x > 0

   assert x > 0
   
   x := x + 1

   //assert exists x0:Int :: x0 > 0 && x == x0+1
   //assert exists x0:Int :: x0 > 0 && x-1 == x0
   assert x-1 > 0

   if (y) {
     assert y && x-1 > 0
     var z: Int
     assert y && x-1 > 0
     x := x + z
     // x == x0 + z <==> x0 == x - z
     assert y && (x-z)-1 > 0
     assert y // we cannot say more after leaving scope
   } else {
    assert !y && x-1 > 0
     x := 42
    // x == 42
    assert !y && 41 > 0
   }
   //assert (y && (x-z)-1 > 0) || (!y && 41 > 0)
   assert (y && true) || (!y && 41 > 0)
}

Task 2 (5 points): Backward reasoning with Viper

For each of the Viper programs below, replace TODO by the weakest predicate such that the contract verifies; try to find a predicate that is as simple as possible.

Hint: Use the Viper verifier to check whether the program verifies for your your proposed predicates.

(a)

method a(x: Int, y: Int) returns (X: Int, Y: Int)
    requires true 
    ensures X == y && Y == x
{
    assert true
    assert y - (y-x) == x
    X := y - x
    assert y - X == x
    assert y == y && y - X == x
    assert y - X + X == y && y-X == x
    Y := y - X
    assert Y+X == y && Y == x
    X := Y + X
    assert X == y && Y == x
    // START HERE
}

(b)

method b() {

    var x: Int 
    var y: Int 

    assume 0 > (x + y) * (y-1) // TODO

    assert x + y > (x + y) * y

    x := x + y 

    assert x > x * y

    y := x * y

    assert x > y
}

(c)

method c() {
    var x: Int 
    var y: Int 

    assume (y > 5 ==> x > 7) && (!(y > 5) ==> y - x > 7)

    assert (y > 5 ==> x > 7) && (!(y > 5) ==> y - x > 7)
    if (y > 5) {
        assert x > 7
        y := x - y
        assert x > 7
    } else {
        assert y - x > 7
        x := y - x
        assert x > 7
    }

    assert x > 7
}

(d)

method d(x: Int) returns (y: Int) 
    requires !(x < 17) || (x < 17 && !(x > 3))
    ensures y % 2 == 0
{
    assert (x < 17 ==> (x > 3 ==> false) && (!(x > 3) ==> true))
            && (!(x < 17) ==> true)
    if (x < 17) {
        assert (x > 3 ==> false) && (!(x > 3) ==> true)
        if (x > 3) {
            assert false
            assert 1 % 2 == 0
            y := 1
            assert y % 2 == 0
        } else {
            assert true
            assert 2 % 2 == 0
            y := 2
            assert y % 2 == 0
        }
        assert y % 2 == 0
    } else {
        assert true 
        assert 6 % 2 == 0
        y := 6
        assert y % 2 == 0
    }
    assert y % 2 == 0
}

Task 3 (7 points): Encoding conditionals

The language PL0 is simplistic and does not support basic statements (see full definition), such as conditionals if (b) { S1 } else { S2 }. Such a statement evaluates the Boolean expression b in the current program state; if the result is true, we execute S1; otherwise, we executes S2.

In terms of our formal operational semantics, the semantics of conditionals is given by the following inference rules:

$$\frac{b,\sigma {⟹}_b\text{true}}{\text{if (b) { S1 } else { S2 }},\sigma ⟹S1,\sigma }\frac{b,\sigma {⟹}_b\text{false}}{\text{if (b) { S1 } else { S2 }},\sigma ⟹S2,\sigma }$$

(a) Define the weakest precondition of conditionals, that is, WP(if (b) { S1 } else { S2 }, Q).

Solution

WP(if (b) { S1 } else { S2 }, Q)
::=
(b ==> WP(S1, Q)) && (b ==> WP(S2, Q))

(b) Define the strongest postcondition of conditionals, that is, SP(P, if (b) { S1 } else { S2 }).

SP(P, if (b) { S1 } else { S2 })
::=
SP(b && P, S1) || SP(!b && P, S2)

(c) Encode the conditional if (b) { S1 } else { S2 } as a PL0 program. That is, write a PL0 program ENC(if (b) { S1 } else { S2 }) that models the effect of a conditional.

Hint: You may write ENC(S1) and ENC(S2) do denote statements the S1 and S2 to which the encoding of conditionals has already been applied.

Solution

ENC(if (b) { S1 } else { S2 })
::=
{
  assume b;
  ENC(S1)
} [] {
  assume !b;
  ENC(S2)
}

(d) Prove that your encoding in (c) is correct in the sense that it yields verification conditions that are logically equivalent to the direct definitions of WP and SP from (a) and (b). That is, show that

• WP(if (b) { S1 } else { S2 }, Q) <==> WP(ENC(if (b) { S1 } else { S2 }), Q) and
• SP(P, if (b) { S1 } else { S2 }) <==> SP(P, ENC(if (b) { S1 } else { S2 })) are valid, where <==> denotes logical equivalence.

Solution

First, we compute WP(ENC(if (b) { S1 } else { S2 }), Q) (read from bottom to top):

{ b ==> WP(S1, Q) && !b ==> WP(S2, Q) }
{
  { b ==> WP(S1, Q) }
  assume b;
  { WP(S1, Q) }  // by I.H.
  ENC(S1)
  { Q }
} [] {
  { !b ==> WP(S2, Q) }
  assume !b;
  { WP(S2, Q) }  // by I.H.
  ENC(S2)
  { Q }
}
{ Q }

Clearly, the result at the top is identical to WP(if (b) { S1 } else { S2 }, Q) as defined in (a).

Second, we compute SP(P, ENC(if (b) { S1 } else { S2 })) (read from top to bottom):

{ P }
{
  { P }
  assume b;
  { b && P }  
  ENC(S1)
  { SP(b && P, S1) } // by I.H.
} [] {
  { P }
  assume !b;
  { !b && P }  
  ENC(S2)
  { SP(b && P, S2) } // by I.H.
}
{ SP(b && P, S1) || SP(!b && P, S2) }

Clearly, the result at the top is identical to SP(P, if (b) { S1 } else { S2 }) as defined in (b).

Task 4 (8 points): Forward reasoning about total correctness

In the lecture, we noticed a difference between weakest preconditions and strongest postconditions: for strongest, the computed verification condition is valid even if the program encounters a runtime error. This corresponds to the notion of partial correctness. By contrast, the verification conditions obtained from computing weakest preconditions consider total correctness, that is, they enforce safety (i.e., the absence of runtime errors) and termination.

To enable forward reasoning about total correctness, we need to compute a second verification condition that enforces safety.

(a) Give a recursive definition of a predicate transformer SAFE: Pred --> PL0 --> Pred such that the predicate SAFE(P, S) is the verification condition that needs to be checked to enforce that starting S on any state in precondition P does not lead to a runtime error. As for strongest postconditions, SAFE(P, S) should reason about statements in forward direction.

Hint: It might help to first express the same safety property in terms of weakest preconditions.

Solution

Intuitively, SAFE(P, S) should be valid for a precondition P and a program S if and only if S does not crash when running it on any initial state that satisfies P.

We go through each PL0 statement S and ask "on which states could an execution of S cause a runtime error?". SAFE(P, S) should then characterize all other states, that is, those that never lead to a crash.

First, we observe (for example by looking at the operational semantics) that variable declarations, assumptions, and assignments never lead to a runtime error. In fact, the only non-composed statement that could cause such an error is a failing assertion.

Hence, we set

SAFE(P, var x) = SAFE(P, x := a) = SAFE(P, assume R) ::= true.

Now, an assertion assert R crashes the program if R does not hold in the current program state. Hence, R must hold for any initial state on which we may run our program, that is, for all states that satisfy precondition P. In other words, if a state satisfies P, then it must also satisfy R. Formally, we define SAFE(P, assert R) ::= P ==> R.

Next, we consider the composed statements S1 [] S2 and S1; S2. The nondeterministic choice is straightforward: S1 [] S2 does not crash if neither S1 nor S2 crashes. Put positively, S1 [] S2 is safe if running S1 and running S2 is safe. Hence, we define SAFE(P, S1 [] S2) ::= SAFE(P, S1) && SAFE(P, S2).

The sequential composition S1; S2 is a little tricky, since there are two cases that could lead to a crash:

1. There is a crash if we run S1 on a state satisfying P; we can prevent that by requiring SAFE(P, S1).
2. There is no crash if we run S1 on a state satisfying P but there is a crash if we run S2 afterward. In other words, there is a crash if we run S2 on some state reached after executing S1 on a state satisfying P, that is, some state described by SP(P, S1). Hence, to prevent such crashes, we require SAFE(SP(P, S1), S2).

Since we need to rule out both of the above cases, we define

SAFE(P, S1;S2) ::= SAFE(P, S1) && SAFE(P, S2)

In summary, the predicate transformer SAFE is given by the following table.

S                       SAFE(P, S)
==================================================================
var x                   true
assert R                P ==> R
assume R                true
x := a                  true
S1; S2                  SAFE(P, S1) && SAFE(SP(P, S1), S2)
S1 [] S2                SAFE(P, S1) && SAFE(P, S2)

(b) Using your definition in (a), prove that, for all PL0 statements S and all predicates P, Q, we have

P ==> WP(S, Q) valid
if and only if
SAFE(P, S) valid and SP(P, S) ==> Q valid

Hint: Proceed by structural induction on the syntax of statements S.

Solution

For simplicity, we denote states by s instead of $\sigma$. Moreover, we write |= R to denote that predicate R is valid, that is, |= R iff s |= R holds for all states s.

We then show by structural induction on the syntax of PL0 statements S that, for all predicates P and Q, we have

(I.H.)  |= P ==> WP(S, Q) if and only if |= SAFE(P, S) and |= SP(P, S) ==> Q       

The case var x

    |= P ==> WP(var x, Q)
iff (Def. of WP)
    |= P ==> forall x :: Q
iff (<>, see below)
    |= (exists x :: P) ==> Q
iff (Def. of SP)
    |= SP(P, var x) ==> Q
iff (Def. of SAFE)
    |= SP(P, var x) ==> Q and |= SAFE(P, var x)

For the step marked with <>, we consider both directions separately:

1. Assume |= P ==> forall x :: Q. Moreover, for an arbitrary, but fixed state s, let s |= (exists x :: P); otherwise there is nothing to show. By assumption, it follows that s |= forall x :: Q. In particular, this means s |= Q. Since we have considered an arbitrary state, we have |= (exists x :: P) ==> Q.
2. Assume |= (exists x :: P) ==> Q. Moreover, for an arbitrary, but fixed state s, let s |= P; otherwise there is nothing to show. Then, s[x := v] |= (exists x :: P) for every integer v (we can choose s(x) as value of x). By assumption, this means s[x := v] |= Q. By the substitution lemma, we have s |= Q[x/v] for every integer v. Hence, s |= forall x :: Q. Since we have considered an arbitrary state, we have |= P ==> forall x :: Q.

The case assume R

    |= P ==> WP(assume R, Q)
iff (Def. of WP)
    |= P ==> R ==> Q
iff
    |= (P && R) ==> Q
iff (Def. of SP)
    |= SP(P, assume R) ==> Q
iff (Def. of SAFE)
    |= SP(P, assume R) ==> Q and |= SAFE(P, assume R)

The case assert R

    |= P ==> WP(assert R, Q)
iff (Def. of WP)
    |= P ==> (R && Q)
iff
    |= P ==> R and |= (P && R) ==> Q
iff (Def. of SAFE and SP)
    |= SAFE(p, assert R) and |= SP(P, assert R) ==> Q

The case x := a

    |= P ==> WP(x := a, Q)
iff (Def. of WP)
    |= P ==> Q[x/a]
iff (<>, see below)
    |= (exists x0 :: P[x/x0] && x == a[x/x0]) ==> Q
iff (Def. of SP)
    |= SP(P, x := a) ==> Q
iff (Def. of SAFE)
    |= SP(P, x := a) ==> Q
    and |= SAFE(P, x := a)

For the step marked with <>, we consider both directions separately:

1. Assume |= P ==> Q[x/a]. Moreover, for an arbitrary, but fixed state s, let s |= (exists x0 :: P[x/x0] && x == a[x/x0]); otherwise there is nothing to show. By assumption and since x0 is not a free variable of P,Q,a, we have |= P[x/x0] ==> Q[x/a][x/0]. Consequently,

         s |= exists x0 :: Q[x/a][x/x0] && x == a[x/x0]
implies  s |= exists x0 :: Q[x/a[x/x0]] && x == a[x/x0]  
implies  s |= exists x0 :: Q
implies  s |= Q

where the last implication follows since x0 is not a free variable of Q.

2. Assume |= (exists x0 :: P[x/x0] && x == a[x/x0]) ==> Q. Moreover, for an arbitrary, but fixed state s, let s |= P; otherwise there is nothing to show. Then s[x0 := s(x)] |= P[x/x0] && x == a[x/x0]. By assumption, this also means s[x0 := s(x)] |= Q && x == a[x/x0]. Hence, by the second conjunct, s[x0 := s(x)][x := s(a[x/x0])] |= Q. Since x0 is not a free variable of Q, this simplifies to s[x := s(a)] |= Q. By the substitution lemma, this means s |= Q[x/a]. Since we have considered an arbitrary state, we have |= P ==> Q[x/a].

The case S1 [] S2

    |= P ==> WP(S1 [] S2, Q)
iff (Def. of WP)
    |= P ==> WP(S1, Q) && WP(S2, Q)
iff
    |= (P ==> WP(S1, Q)) && (P ==> WP(S2, Q))
iff (I.H. twice)
    |= (SP(P,S1) ==> Q
    and |= SAFE(P, S1)
    and |= (SP(P,S2) ==> Q
    and |= SAFE(P, S2)
iff (Def. of SAFE)
    |= (SP(P,S1) ==> Q
    and |= (SP(P,S2) ==> Q
    and |= SAFE(P, S1 [] S2)
iff
    |= ((SP(P,S1) || SP(P,S2)) ==> Q
    and |= SAFE(P, S1 [] S2)
iff (Def. of SP)
    |= SP(P,S1 [] S2) ==> Q
    and |= SAFE(P, S1 [] S2)

The case S1;S2

    |= P ==> WP(S1;S2, Q)
iff (Def. of WP)
    |= P ==> WP(S1, WP(S2, Q))
iff (I.H.)
    |= SP(P, S1) ==> WP(S2, Q)
    and |= SAFE(P, S1)
iff (I.H.) 
    |= SP(SP(P, S1), S2) ==> Q
    and |= SAFE(SP(P, S1), S2)
    and |= SAFE(P, S1)
iff (Def. of SP and SAFE)
    |= SP(P, S1;S2) ==> Q
    and |= SAFE(P, S1;S2)

Hence, the claim holds by the principle of structural induction.

Satisfiability Modulo Theories

Preconditions

Files:     [Slides]     [Code skeletons]

We will mostly work with Z3 during this lecture, so please make sure that you can run Z3 on your machine; installation instructions are found here.

Furthermore, if you have not already done so, you may want to refresh your background on first-order predicate logic, preliminaries.

Postconditions

Files:     [Slides after class on Sep. 8]     [Code after class on Sep. 8]

Files:     [Full Slides with solutions]     [Full code examples with solutions]

Update: The final slides do not treat equality (=) as a relational symbol. Instead, as in the reading assignment, we treat equality as a fixed interpreted symbol that is always available and has the canonical meaning. Equality is thus not part of the signature anymore; you can always use it. We removed it from signatures in the final slides and on the course page.

Of course you will not be punished if your homework uses the old treatment of equality.

What you should have learned after completing chapter 2:

• Basics of propositional and (many sorted) first-order logic (FOL)
• What Satisfiability Modulo Theories means
• How to use read and write specifications using FOL over built-in or custom theories
• How to write simple axiom systems
• How to encode problems and theorems to instances of the SAT/SMT problem and solve them with existing solvers

Homework

Reading assignment

The book by Ebbinghaus, Flum, and Thomas pdf gives a detailed introduction to first-order predicate logic. It uses almost the same notation as in the lecture. The main exceptions are:

• For substitution, we write $\mathfrak{I}[x:=a]$ instead of $\mathfrak{I}\frac{a}{x}$.
• For equality, we write $=$ instead of $\equiv$.
• We denote signatures by Σ instead of S (which we use for program statements).
• Formulas F are denoted by $\phi$ and axiomatic systems AX are denoted by $\Phi$.
• Satisfiability modulo theory is denotes as $\Phi \models \phi$ in the book, where $\Phi$ represents the axiomatic system, i.e. it is a set of Σ-sentences.

We list parts of the book that cover the concepts discussed during the lecture below. We recommend reading some of those parts unless you are already closely familiar with first-order logic.

• Chapter II introduces the syntax of FOL in more detail
  • Chapter II.3: Σ-terms, Σ-formulas
  • Chapter II.5: Free variables, Σ-sentences
• Chapter III discusses the semantics of FOL
  • Chapter III.1: Σ-structures, signatures, and interpretations
  • Chapter III.3 discusses the satisfaction relation $\models$ in more detail
  • The book presents satisfiability and validity without taking a theory into account. The notion that a formula F is valid modulo a theory Th given by an axiomatic system AX corresponds to the notation AX |= F in the book. You can read the beginning of Chapter III.4 (p. 32-33) to take another view on these concepts. Our notion of validity modulo theories is found in Lemma 4.4: $\Phi \models \phi$ iff not $\text{Sat}\Phi \cup \{\phi \}$. In words, $\phi$ is valid modulo the theory given by axiomatic system $\Phi$ if and only if $\neg \phi$ is satisfiable modulo the theory given by axiomatic system $\Phi$.
  • Chapter III.6 gives examples of axiomatic systems that characterize structures corresponding to various mathematical concepts.

Furthermore, the literature page gives optional references with more information about SAT/SMT solving. In particular, the Z3 tutorials might be useful to you when working on the homework tasks.

The next lecture will be concerned with building practical verifiers. There is no additional material for you to prepare, but make sure that you can work with the concepts and tools we have used lecture 1 and lecture 2.

Tasks

Submission deadline: Thursday, September 22, 12:59 (right before the lecture).

Notice that you have two weeks for completing the homework. The material needed for solving tasks 3 and 4 will be covered in the class on September 15.

Please submit your solutions by pushing all relevant files to the GitLab repository assigned to your group. If you have not been assigned a repository yet, contact the teacher.

Task 1 (2 points): First-order logic

Consider the signature Σ = (Int, +, *, 0, 1), where +, *: Int x Int -> Int are binary function symbols and 0, 1: Int are constant function symbols.

Give a Σ-formula F expressing that $x<y$ holds modulo the theory of Peano arithmetic (without using the symbol <!). That is, for every interpretation $\mathfrak{I}$ in which all symbols have the canonical meaning, $\mathfrak{I}\models F$ should hold if and only if the integer $\mathfrak{I}(x)$ is strictly less than $\mathfrak{I}(y)$.

Your formula should not have any free variables other than $x$ and $y$.

Task 2 (5 points): Axiomatic Systems

In the lecture, we introduced axiomatic systems to specify only those Σ-structures that we are interested in. The goal of this task is to find suitable axiomatic systems for a few interesting classes of Σ-structures.

First, consider the signature Σ = (V, E), where V is some sort. Moreover, E: V x V is a binary relational symbol.

(a) Give an axiomatic system AX describing all undirected graphs without self-loops.

(b) Give an axiomatic system AX describing all structures Σ = (V, E) in which E represents a total order of the elements of V.

(c) Give an axiomatic system AX describing all structures with more than two elements, that is, those structures Σ = (V, E) such that |V| > 2.

Now, consider the signature Σ = (Array, Int, get, put), where Array and Int are sorts. Moreover, get: Array x Int -> Int and put: Array x Int x Int -> Array are function symbols.

(d) Give an axiomatic system AX describing (unbounded) arrays (elements of sort Array) of integers (elements of sort Int) using the above signature. Here, get(A, i) represents the i-th value of array A and put(A, i, v) represents the array which is the same as array A but with the i-th value set to v. Your axiomatic system should ensure that two arrays are considered equal if they contain the same elements.

Hint: Read the task carefully.

Task 3 (3 points): Using an SMT solver

A large Danish company currently produces three kinds of products, let's call them product A, B, and C. The company wishes to reduce overhead by producing only two kinds of products in the future.

Your task is to use Z3 to evaluate whether this is possible given the companies production constraints listed below.

• The company needs to produce at least 100 products (of any kind) within 3 hours.
• The company needs to produce at least 5 products of kind A or kind B.
• The company needs to produce at least 10 products of kind C.
• To produce a product of kind A, B, and C, the company needs 1, 2, and 5 minutes, respectively.
• To produce a product of kind A, B, and C, the company needs to invest 3000, 2000, and 1000 DKK, respectively.
• The company wants to invest at most 300000 DKK.

Submit your encoding of the above problem in Z3 (using SMTLIB or one of the APIs, e.g. pySMT); briefly explain your constraints using inline comments.

Task 4 (20 points): Akari

For this task, we consider a puzzle game with simple rules and challenging solutions called "Akari" or "Light Up". The rules are as follows:

• The game is played on a rectangular grid of walls (black tiles) and empty (white) tiles.
• Initially the whole grid is dark.
• The goal is to place lightbulbs on some of the empty tiles until all non-wall tiles are lit.
• Every lightbulb shines light in the 4 cardinal directions (up, down, left, right) until the light is stopped by a wall.
• Two lightbulbs are not allowed to shine light on each other.
• Some wall tiles may have a number (typically between 0 and 4) assigned to it, which indicates how many lightbulbs must be placed in the adjacent empty tiles.

If you want to get a feeling for the game, you can also play it online. Furthermore, here is a collection of example puzzles, together with solutions for the first few puzzles:

Your task is to implement a program that utilizes Z3 to solve arbitrary Akari puzzles, such as the ones illustrated above.

The above examples each have a unique solution but, in general, your implementation should find some solution. If there is no solution, it should report that as well.

Make sure that your code is well-documented. In particular, explain what each constraint that you give to the SMT solver means.

You can choose any language that you want to use. We provide you with two code skeletons, one using the python Z3 bindings and one using the rust Z3 bindings, respectively. Both code skeletons contain:

• An explanation of how puzzles are represented.
• An explanation of how solutions are represented.
• The function validate_solution which takes a puzzle and a solution and checks whether the solution is correct. You can use this function, together with the seven puzzles from above, which are also provided in the file, to test your implementation.
• An unimplemented function solve that you should implement.

Files: Skeletons for Akari

Further reading (optional)

We give a list of books, papers, and webpages with additional information of how SAT/SMT solvers work as well as tutorials for using them together with various programming languages.

For a general introduction to mathematical logic, some references are found in the preliminaries.

Tutorials & Documentation

• Tutorial for using Z3 through the SMTLIB-2 language
• Tutorial for using Z3 through its Python API
• Advanced tutorial on Z3 using the Python API
• Collection of intriguate example problems solved using SAT/SMT solvers
• Detailed documentation of the SMTLIB-2 format

More on SAT Solvers

A comprehensive introduction to satisfiability solving is found in the handbook of satisfiability:

Handbook of satisfiability. Armin Biere. 2009.

The original algorithm for SAT solving is DPLL: Davis-Putnam-Logemann-Loveland. You can read more about it in the original paper.

A machine program for theorem-proving. Martin Davis, George Logemann, and Donald Loveland. 1962.

Modern SAT solvers typically use a different algorithm, called Conflict-Driven Clause Learning (CDLC):

GRASP – A New Search Algorithm for Satisfiability. João P. Marques Silva and Karem A. Sakallah. 1996.

For a comparison of existing SAT solvers, we refer to the annual SAT competition.

More on SMT Solvers

A comprehensive introduction to SMT solving is found in the following book:

Decision procedures : an algorithmic point of view. Daniel Kroening and Ofer Strichman. 2008.

The book's website also provides supplementary material, for example slides for selected topics.

There are also excellent courses that focus on the theory, implementation, and usage of SMT solvers:

• Leonardo de Moura. SMT Solvers: Theory and Implementation.
• Clark Berret. SMT Solvers: Theory and Practice.
• Erika Abraham. Satisfiability Checking

Solutions to Homework Tasks

Task 1 (2 points): First-order logic

Consider the signature Σ = (Int, +, *, 0, 1), where +, *: Int x Int -> Int are binary function symbols and 0, 1: Int are constant function symbols.

Give a Σ-formula F expressing that $x<y$ holds modulo the theory of Peano arithmetic (without using the symbol <!). That is, for every interpretation $\mathfrak{I}$ in which all symbols have the canonical meaning, $\mathfrak{I}\models F$ should hold if and only if the integer $\mathfrak{I}(x)$ is strictly less than $\mathfrak{I}(y)$.

Your formula should not have any free variables other than $x$ and $y$.

Solution

Intuitively, $x<y$ holds iff we can find a natural number $z>0$ such that $x+z==z$ is true.

If we assume, for the moment, that Σ would use the sort Nat of natural numbers instead of arbitrary integers, then we could use the formula

exists z: Nat :: !(z == 0) && x + z == y

However, we need to consider the sort Int of arbitrary integers. One approach is to use the above formula, with z no of sort Int, and then adding a constraint that z is a natural number.

For example, we can express this property using Lagrange's four-square theorem, which states that every natural number can be represented as the sum of four (necessarily non-negative) integer squares.

This yields the following formula

exists z:Int, a:Int, b:Int, c: Int, d: Int ::
    z == a*a + b*b + c*c + d*d &&
    !(z == 0) && x + z == y

Task 2 (5 points): Axiomatic Systems

In the lecture, we introduced axiomatic systems to specify only those Σ-structures that we are interested in. The goal of this task is to find suitable axiomatic systems for a few interesting classes of Σ-structures.

First, consider the signature Σ = (V, E), where V is some sort. Moreover, E: V x V is a binary relational symbol.

(a) Give an axiomatic system AX describing all undirected graphs without self-loops.

Solution

// the edge relation E is symmetric for undirected graphs
forall x: V, y: V :: E(x,y) ==> !(x == y)

// self-loops are not allowed
forall x: V, y: V :: E(x,y) ==> E(y,x)

(b) Give an axiomatic system AX describing all structures Σ = (V, E) in which E represents a total order of the elements of V.

Solution

// reflexivity
forall x:V :: E(x,x)

// antisymmetry
forall x:V, y:V :: E(x,y) && E(y,x) ==> x = y

// transitivity
forall x: V, y: V, z: V :: E(x,y) && E(y,z) ==> E(x,z)

// totality
forall x: V, y: V :: E(x,y) || E(y,x)

(c) Give an axiomatic system AX describing all structures with more than two elements, that is, those structures Σ = (V, E) such that |V| > 2.

Solution

exists x: V, y: V, z: V :: !(x == y) && !(x == z) && !(y == z)

Now, consider the signature Σ = (Array, Int, get, put), where Array and Int are sorts. Moreover, get: Array x Int -> Int and put: Array x Int x Int -> Array are function symbols.

(d) Give an axiomatic system AX describing (unbounded) arrays (elements of sort Array) of integers (elements of sort Int) using the above signature. Here, get(A, i) represents the i-th value of array A and put(A, i, v) represents the array which is the same as array A but with the i-th value set to v. Your axiomatic system should ensure that two arrays are considered equal if they contain the same elements.

Hint: Read the task carefully.

Solution

We first add an axiom that we retrieve the same values that we have previous put into an array:

forall A:Array :: 
    forall i:Int, v::Int ::
        get(put(A,i,v), i) == v

When retrieving a value, the outermost put function may also consider a different index. To ignore such a case, we can axiomatize that putting in values is commutative as long as we use different array indices:

forall A:Array :: 
    forall i:Int, v:Int, j:Int, w:Int ::
        i != j ==> put(put(A,i,v),j, w) == put(put(A,j,w),i,v)

Alternatively, we could explicitly ignore different indices for the get function:

forall A:Array :: 
    forall i:Int, v:Int, j:Int ::
        i != j ==> get(put(A,i,v),j) == get(A,j)

The last part requires careful reading of the task: "your axiomatic system should ensure that two arrays are considered equal if they contain the same elements".

The description only requires that two arrays have the same set of elements; the indices and cardinalities do not matter. A corresponding axiom would be

forall A:Array, B:Array ::
    (forall i:Int :: exists j:Int :: get(A,i) == get(B,j))
        ==> A == B

This axiom states what the task requires. However, we may actually want to also take the order and cardinalities into account when axiomatizing an actual array. We can use the following axiom for that:

forall A:Array, B:Array ::
    (forall i:Int :: get(A,i) == get(B,i))
        ==> A == B

Task 3 (3 points): Using an SMT solver

A large Danish company currently produces three kinds of products, let's call them product A, B, and C. The company wishes to reduce overhead by producing only two kinds of products in the future.

Your task is to use Z3 to evaluate whether this is possible given the companies production constraints listed below.

• The company needs to produce at least 100 products (of any kind) within 3 hours.
• The company needs to produce at least 5 products of kind A or kind B.
• The company needs to produce at least 10 products of kind C.
• To produce a product of kind A, B, and C, the company needs 1, 2, and 5 minutes, respectively.
• To produce a product of kind A, B, and C, the company needs to invest 3000, 2000, and 1000 DKK, respectively.
• The company wants to invest at most 300000 DKK.

Submit your encoding of the above problem in Z3 (using SMTLIB or one of the APIs, e.g. pySMT); briefly explain your constraints using inline comments.

Solution

; number of products of kind A, B, and C, respectively
(declare-const A Int)
(declare-const B Int)
(declare-const C Int)

; produce at least 100 products (of any kind) 
; within 3 hours (we ignore everything after that)
(assert (>= (+ A B C) 100 ))

; To produce a product of kind A, B, and C, the company needs 1, 2, and 5 minutes
; we cut off production after 180 minutes (3h)
(assert (>= 180 (+ (* A 1) (* B 2) (* C 5))))

; The company needs to produce at least 5 products of kind A or kind B.
(assert (or (<= 5 A) (<= 5 B)))
; ambiguity: could also be understood as (assert (<= 5 (+ A B)))

; The company needs to produce at least 10 products of kind C.
(assert (<= 10 C))

; To produce a product of kind A, B, and C, 
; the company needs to invest 3000, 2000, and 1000 DKK
; The company wants to invest at most 300000 DKK.
(assert (>= 300000 (+ (* A 3000) (* B 2000) (* C 1000))))

; a model now gives as the production numbers for each kind
; to check whether the company can omit a product, we can
; additionally assert that 0 products of one kind are produced
; and see if the formula remains satisfiable.

(push)
(echo "Can we drop producing A? (unsat means no)")
(assert (= A 0))
(check-sat)
(pop)

(push)
(echo "Can we drop producing B? (unsat means no)")
(assert (= B 0))
(check-sat)
(pop)

(push)
(echo "Can we drop producing B? (unsat means no)")
(assert (= C 0))
(check-sat)
(pop)

Task 4 (20 points): Akari

For this task, we consider a puzzle game with simple rules and challenging solutions called "Akari" or "Light Up". The rules are as follows:

• The game is played on a rectangular grid of walls (black tiles) and empty (white) tiles.
• Initially the whole grid is dark.
• The goal is to place lightbulbs on some of the empty tiles until all non-wall tiles are lit.
• Every lightbulb shines light in the 4 cardinal directions (up, down, left, right) until the light is stopped by a wall.
• Two lightbulbs are not allowed to shine light on each other.
• Some wall tiles may have a number (typically between 0 and 4) assigned to it, which indicates how many lightbulbs must be placed in the adjacent empty tiles.

If you want to get a feeling for the game, you can also play it online. Furthermore, here is a collection of example puzzles, together with solutions for the first few puzzles:

Your task is to implement a program that utilizes Z3 to solve arbitrary Akari puzzles, such as the ones illustrated above.

The above examples each have a unique solution but, in general, your implementation should find some solution. If there is no solution, it should report that as well.

Make sure that your code is well-documented. In particular, explain what each constraint that you give to the SMT solver means.

You can choose any language that you want to use. We provide you with two code skeletons, one using the python Z3 bindings and one using the rust Z3 bindings, respectively. Both code skeletons contain:

• An explanation of how puzzles are represented.
• An explanation of how solutions are represented.
• The function validate_solution which takes a puzzle and a solution and checks whether the solution is correct. You can use this function, together with the seven puzzles from above, which are also provided in the file, to test your implementation.
• An unimplemented function solve that you should implement.

Files:

Skeletons for Akari

Solution with comments

Building Automated Verifiers

Preconditions

Files:     [Slides]     [Code examples]

Postconditions

Files:     [Slides with solutions]     [Code examples]

Notice that some slides have been corrected after class.

What you should have learned after completing chapter 3:

• Explain the overall architecture of automated verifiers based on the principle to treat "verification as compilation"
• Explain what an encoding in the toolchain of a verifier means and what desirable properties, for example soundness, completeness, explainabilit, and efficiency, mean
• How to justify that an encoding is sound or complete
• How to obtain more efficient verification conditions through program transformations, specifically dynamic single assignment form (DSA) and passification
• Strategies for systematically localizing errors if verification fails

Homework

There is no explicit homework that you need to submit. Instead, use this week to work on the first project.

Reading assignment

We will consider programs with loops and procedures in chapter 4. For that, we need a few concepts from domain theory, which you might have seen in other courses, for example program analysis, or not.

As a preparation for next class, please go over the background material on domain theory such that we can have an informed discussion about loops and procedures in class. You can use this form for questions and unclarities about the reading material. I will try to address your questions in class.

Loops & Procedures

This module is split into two parts, see loops and procedures.

Loops

Preconditions

Files:     [Slides]     [Code examples]

As a preparation for next class, please go over the background material on domain theory such that we can have an informed discussion about loops and procedures in class. You can use this form for questions and unclarities about the reading material. I will try to address your questions in class.

Postconditions

Files:     [Slides with solutions]     [Code examples with solutions]

What you should have learned after completing chapter 4.1:

• If we allow for arbitrary predicates, then the precise weakest precondition of a loop is given by a fixed point, which states that the weakest precondition equals the weakest precondition of unfolding the loop.
• When reasoning about total correctness, the weakest precondition corresponds to the least fixed point of said loop unfolding.
• When reasoning about partial correctness, that is if we do not care about termination, then the weakest liberal precondition corresponds to the greatest fixed point of said loop unfolding.
• While we can, in principle, represent the above fixed points by predicates in the syntax allowed by PL0, it is typically far too complicated for automated verification tools. We thus use proof rules for reasoning about loops without determining the exact weakest precondition.
• We typically split the task of verifying loops into two: we use invariants for showing partial correctness and variants to show termination. The correctness of these constructs is justified by reasoning about the fixed points discussed above.
• A loop invariant is a predicate that must hold before every loop iteration. You should be able to find sufficiently strong loops invariants to verify that a program with a loop satisfies its contract.
• A variant is an expression over some well-founded ordering that decreases in every loop iteration. If a variant exists, then the loop terminates. You should be able to find simple variants (e.g. using the ordering < over natural numbers) for a given loop.
• You should be able to automate reasoning with loop invariants and variants by encoding these concepts into PL0.

Homework

Tasks

Submission deadline: Thursday, October 6, 12:59 (right before the lecture).

Please submit your solutions by pushing all relevant files to the GitLab repository assigned to your group. If you have not been assigned a repository yet, contact the teacher.

Task 1 (5 points): Slow square roots

The following Viper program attempts to compute the integer square root of some natural number n. Find a suitable invariant for the line marked with TODO such that the program verifies.

Hint: Notice that the specification admits programs that do not enforce the computation of the integer square root of n. We will address this in class. You should still find a suitable invariant.

method int_sqrt() {
    var n: Int
    assume n >= 0

    var res: Int

    res := 0
    while ((res + 1) * (res + 1) < n)
        invariant false // TODO
    {
        res := res + 1
    }

    assert res * res <= n
        && n <= (res + 1) * (res + 1) 
}

Task 2 (5 points): Fast square roots

The following Viper program attempts to compute the integer square root of some natural number n more efficiently. Find a suitable invariant for the line marked with TODO such that the program verifies.

Hint: Notice that the specification admits programs that do not enforce the computation of the integer square root of n. We will address this in class. You should still find a suitable invariant.

method int_sqrt_fast() {
    var n: Int 
    assume n >= 0

    var res: Int

    res := 0
    var x: Int := 1
    while (x < n)
        invariant false // TODO
    {
        x := x + 2 * res + 3
        res := res + 1
    }

    assert res * res <= n
        && n <= (res + 1) * (res + 1) 
}

Task 3 (10 points): Square without multiplication

Implement and verify the method below such that it returns the square of any given non-negative integer n.

Your implementation must not use recursion or any arithmetic other than constants and +1. That is, x := 0 and x := x + 1 are allowed. However, x := y + z, x := x * y, and x := 2 * x are not allowed.

You may still use arbitrary arithmetic in assertions and invariants.

method square(n: Int) returns (res: Int)
    requires n >= 0
    ensures res == n * n
{
    // TODO
}

Procedures

Preconditions

Files:     [Slides]     [Code examples]

Postconditions

Files:     [Slides with solutions]     [Code examples with solutions]

Notice that some slides have been corrected after class.

What you should have learned after completing chapter 4.2:

• The semantics of recursive procedures can be formalized in turns of higher-order fixed points.
• We reason modularly about procedure calls, that is, we rely solely on the procedure contract without inspecting its implementation.
• For partial correctness reasoning, this yields a simple approach: try to proof the specification for the procedure and use the contracts whenever we encounter a procedure call.
• In contrast to loops, we cannot strengthen procedure contracts whenever we encounter a new client. It is thus very important to support framing: properties that are not affected by a call should be preserved.
• Similarly to loops, we use variants to prove that a procedure terminates.
• You should be able to automate modular reasoning about procedures and termination proofs with variants by encoding these concepts into PL0.

Domain theory

When reasoning about loops and procedures, we typically need to reason about fixed points; a fixed point of a function f is some x such that f(x) = x. This kind of reasoning requires a few definitions and results from domain theory, particularly complete lattices, monotone functions, the Knaster-Tarski fixed point theorem, continuous functions, and Kleene's fixed point theorem.

We briefly summarize the main definitions and results that we will need in the course. For an in-depth introduction, we refer to the literature at the end of this page.

We will see more examples in class. You can use this form for questions and unclarities about the reading material. I will try to address your questions in class.

Partial orders

In the following let D be a non-empty set and ⊑: D x D a binary relation over the elements of D.

We call the pair `(D, ⊑) a partial order (or a poset: partially ordered set) if for all

• ⊑ is reflexive: for all a ∈ D, a ⊑ a;
• ⊑ is transitive: for all a,b,c ∈ D, if a ⊑ b and b ⊑ c, then a ⊑ c; and
• ⊑ is antisymmetric: for all a,b,c ∈ D, if a ⊑ b and b ⊑ a, then a = b.

For example, $(\mathbb{Z},\le )$ and $(\mathbb{N},\le )$ - the sets of integers and natural numbers with the usual ordering $\le$ - are partial orders. Another example with perhaps a less obvious order are predicates:

Example. Recall that we initially did not fix a specific syntax for predicates. Instead, we considered the set

Pred ::= { P | P: States -> Bool }

consisting of arbitrary mappings from states to Bool = {true, false}. We can order predicates by pointwise logical implication, i.e. for ⊑ ::= ==>. More formally, for for two predicates P, Q in Pred, we define

P ==> Q iff for all states s, the predicate P(s) ==> Q(s) maps to true.

Lemma. (Pred, ==>) is a partial order.

We leave the proof, i.e. showing that ==> is indeed reflexive, transitive, and antisymmetric as an exercise.

Complete lattices

Let (D, ⊑) be a partial order and let S ⊆ D be any subset of D.

• We call an element d ∈ D an upper bound of S if it is larger than every element of S, that is, iff s ⊑ d holds for all d ∈ D.
• If there is no other upper bound of S that is smaller than d, then d is the least upper bound of S; formally: for all d ∈ D, if d' is an upper bound of S, then d ⊑ d'.
• We also call the least upper bound (with respect to the considered ordering relation ⊑) the supremum of S and denote it by sup S.
• Analogously, d ∈ D is a lower bound of S if it is smaller than every element of S, that is, iff d ⊑ s holds for all d ∈ D.
• If there is no other lower bound of S that is larger than d, then d is the greatest bound of S; formally: for all d ∈ D, if d' is a lower bound of S, then d' ⊑ d.
• We also call the greatest lower bound (with respect to the considered ordering relation ⊑) the infimum of S and denote it by inf S.

For example, consider the partial order (Pred, ==>) and the subset

S ::= {x == 1, x == 2, x == 3}

Then x >= 1 is an upper bound of S since it is implies by each element. However, it is not the least upper bound; that is x == 1 || x == 2 || x == 3.

Not every subset of a partial order has a least upper bound or a greatest lower bound. For example, consider the partial order $(\mathbb{N},\le )$ and the subset $S::=\mathbb{N}$. There is no natural number that is larger or equal to every natural number.

Complete lattice. A partial order (D, ⊑) where every subset S ⊆ D has a least upper bound in D is called a complete lattice.

In fact, if (D, ⊑) is a complete lattice, then every subset S ⊆ D automatically also has a greatest lower bound in D. Furthermore, it follows that D has a unique smallest element, called bot (bottom), which is given by

bot = sup {} = inf D

D also has a unique largest element, called top, which is given by

top = inf {} = sup D

Notice that neither $(\mathbb{Z},\le )$ nor $(\mathbb{N},\le )$ can be complete lattices, since they have no largest element. By contrast, $(\mathbb{N}\cup \{\infty \},\le )$ is a complete lattice: for every subset S, the supremum of S is the maximal element of S if such an element exists; otherwise, the supremum sup S is $\infty$.

Lemma. (Pred, ==>) is a complete lattice.

To show that the partial order (Pred, ==>) is a complete lattice, we need to find a suitable least upper bound in Pred for every subset S ⊆ Pred of predicates. The main idea is that the supremum sup S maps a state s to true if there exists a predicate P ∈ S such that P(s) is true; if no such predicate exists, sup S maps s to false. Formally, for all states s,

(sup S)(s) ::= exists P:Pred :: P ∈ Pred && P(s) == true

Clearly this definition yields an upper bound: whenever a predicate in S is true, so is sup S. We leave the proof that sup S is indeed the least upper bound as an exercise.

Question: What is the smallest (resp. the largest) element of the complete lattice (Pred, ==>)?

Monotone functions

Let (D, ⊑) be a complete lattice and let f: D -> D be a function mapping elements in D to elements in D. The function f is monotone if it preserves the ordering ⊑. Formally, f is monotone iff

f is monotone 
iff
for all a,b ∈ D, a ⊑ b implies f(a) ⊑ f(b)

For example, the function given by f(x) ::= x+1 is monotone for the complete lattice $(\mathbb{Z}\cup \{-\infty ,\infty \},\le )$. By contrast, the function given by f(x) ::= -x is not.

Lemma. For every PL0 statement S, the mapping from postconditions Q to the weakest precondition of S and Q, that is the fucntion WP(S, .): Pred -> Pred, is monotone.

The proof is by structural induction on the structure of PL0 programs and left as an exercise.

Fixed points of monotone functions

Let (D, ⊑) be a complete lattice. Moreover, let f: D -> D be a monotone function.

• We call d ∈ D a fixed point of f if f(d) = d.
• Every element d in D such that f(d) <= d holds is called a pre-fixed point of f.
• Conversely, every element d in D such that d <= f(d) holds is called a post-fixed point of f.

Every fixed point of f is thus both a pre-fixed and a post-fixed point of f.

In general, a function can have no, exactly one, or arbitrarily many fixed points:

• The function f(x) ::= -x has no fixed point when considering the complete lattice $(\mathbb{Z}\cup \{-\infty ,\infty \},\le )$, since the result always oscillates between two possible results.
• For the function f(x) ::= x, every element in its domain is a fixed point.
• For the function f(x) ::= x + 1 and the complete lattice $(\mathbb{N}\cup \{\infty \},\le )$, there is only one fixed point: we have f(∞) = ∞.

The Tarski-Knaster fixed point theorem ensures that every monotone function f: D -> D over a complete (D, ⊑) has at least one fixed point. Even better, the theorem gives characterizations of the least fixed point and the greatest fixed point of f: the least fixed point is the smallest pre-fixed point and the greatest fixed point is the largest post-fixed point.

Knaster-Tarski Fixed Point Theorem. Let (D, ⊑) be a complete lattice and let f: D -> D be a monotone function.

Then the least fixed point of f, fix(f) for short, is given by

fix(f) = inf { d ∈ D | f(d) ⊑ d }.

Furthermore, the greatest fixed point of f, FIX(f) for short, is given by

FIX(f) = sup { d ∈ D | d ⊑ f(d) }.

For example, for the identify function f(x) ::= x, the least fixed point is

fix(f) = inf { d ∈ D | f(d) ⊑ d } = inf { d ∈ D } = bot

A proof is found, for example, in Proposition 2.1.7 of Samson Abramsky and Achim Jung: Domain Theory, available online.

Fixed points of continuous functions

The Tarski-Knaster theorem gives us a theoretical characterization of least and greatest fixed points. However, it does not explain how we could try to compute them, for example by applying f repeatedly until we reach a fixed point. For such a computational characterization, we need a stronger notion than monotonicity, which admits swapping function application and taking the supremum:

A function f: D -> D is continuous iff for every subset S ⊆ D, we have

sup { f(d) | d in S } = f( sup S )

In particular, every continuous function is also monotonous. Hence, it has a least and greatest fixed point (which may be identical).

Lemma. For every PL0 program S, the function WP(S, .): Pred -> Pred is continuous.

For continuous functions, Kleene's fixed point theorem allows us to characterize the least and greatest fixed point through iterative application:

Kleene fixed point theorem. Let (D, <=) be a complete lattice. Moreover, let f: D -> D be a continuous function. Then:

fix(f) ::= sup { f^n(bot) | n in Nat }

and

FIX(f) ::= inf { f^n(top) | n in Nat },

where f^n denotes the n-fold application of f, that is,

f^0(d) ::= d and f^{n+1}(d) ::= f^{n}(f(d)).

Notice that Kleene's fixed point theorem does not mean that we will reach the least or greatest fixed point after finitely many function applications. It is possible, that we might actually have to apply f infinitely often and only reach the fixed point in the limit.

This is different from fixed point theorems you might have encountered in program analysis or other courses, where additional constraints (e.g. finite height) guarantee that one reaches the fix point after finitely many steps.

For example, consider the function f given by f(x) ::= x+1 over the complete lattice $(\mathbb{N}\cup \{\infty \},\le )$. We can iteratively apply f to the least element bot to approximate the least fixed point:

f^0(bot) = bot = 0
f^1(bot) = f(0) = 0 + 1 = 1
f^2(bot) = f(f(0)) = f(1) = 1 + 1 = 2
f^3(bot) = f(f(f(0)) = f(2) = 3
...
f^n(bot) = f(f^{n-1}(bot)) = f(n-1) = n 

We can continue apply f forever. After each application, we get slightly closer to the function's unique fixed point, ∞, but we never reach it.

Further reading

Chapter 8 of Glynn Winskel: The formal semantics of programming languages - an introduction. Foundation of computing series, MIT Press 1993, available online.

Chapter 5 of Hanne Riis Nielson, Flemming Nielson: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science, Springer 2007, available online.

A thorough introduction to domain theory is found in

Samson Abramsky and Achim Jung: Domain Theory, available online.

Chapter 2 roughly covers the results presented above.

Data types

Preconditions

Files:     [Slides]     [Code examples]

Postconditions

Files:     [Slides with solutions]     [Code examples with solutions]

What you should have learned after completing chapter 5:

• We can add new datatypes and operations to our verifier by adding custom axiomatizations, which correspond to domains in Viper.
• Verification tools often already provide various built-in axiomatizations for common mathematical types like sets and sequences.
• Verification often requires defining a suitable mathematical vocabulary first. It is often convenient to define such vocabulary as functional programs - a shortcut for specific axiomatizations based on the definitional axiom of a function.

Verifier tactics

Preconditions

Files:     [Slides]     [Code examples]

We will use the second half of this class to work on some hands-on verification problems.

Postconditions

Files:     [Slides with solutions]     [Code examples with solutions]

What you should have learned after completing chapter 6:

• Identify possible bottlenecks in automated verifiers introduced through incomplete reasoning about quantifiers, e.g. matching loops.
• The basics of Heuristic quantifier instantiation using pattern-based e-matching.
• Pragmatic strategies for dealing with verification bottlenecks, such as manually providing ground terms, limited functions (bounding the unfolding depth of functions), supplying suitable triggering patterns, and introducing ghost code.
• Writing and proving lemmas as ghost methods.
• Using an automated verifier for proving simple algorithms correct.

Heaps and Objects

Preconditions

Files: [Slides] [Code examples]

Postconditions

Files: [Slides with solutions] [Code examples with solutions]

What you should have learned after completing chapter 7:

• Challenges arising from reasoning about heap-manipulating programs, particularly aliasing and framing.
• How the heap is modeled
• Rules for reasoning about heap updates
• Permissions and the separating conjunction; two concepts that enable efficient reasoning about memory safety, allow concise specifications that there are no aliases, and enable framing in the presence of a heap.
• Working with permissions using the permission-aware analogues of assume and assert statements: inhale and exhale
• Encodings of the above concepts

Abstraction

Preconditions

Files: [Slides] [Code examples]

Postconditions

Files: [Slides] [Code examples]

What you should have learned after completing chapter 8:

• How to use predicates as a mechanism for writing specifications about permission transfer that respects information hiding and supports reasoning about unbounded dynamic data structures.
• How to use representation invariants to specify consistency conditions for data structures and how to verify their maintenance by folding and unfolding predicates.
• Methodologies for writing abstract functional specifications through data abstraction, particularly using ghost code or heap dependent abstraction functions.

Permission models

Preconditions

Files: [Slides] [Code examples]

Postconditions

Files: [Slides with solutions]

[Code examples]

What you should have learned after completing chapter 9:

• How to use fractional permissions to specify and verify data structure with complex sharing, for example, doubly-linked lists or data structures with caching.
• How to extend the encoding of the heap and permissions to allow for fractional permissions.
• Strategies for permission accounting, for example wildcard permissions and permission fractions stored in ghost field.
• Strengths and weaknesses of using recursive predicates for reasoning about complex data structures.
• How to use quantified permissions to verify iterative traversals and random access data structures.

Concurrency

Preconditions

Files: [Slides] [Code examples]

Postconditions

Files: [Slides with solutions] [Code examples with solutions]

Frontends

Files: [Slides] [Code examples]

Project A

Deadline: October 27, 23:59

The project can be solved in many different ways. It is important that you can reasonably justify your design decisions. Feel free to ask for clarification if you are unsure about a task or your approach.

Submission: push your solution to the GitLab repository of your homework group. The latest push before the deadline will be considered as your submission.

Task

Your task is to use the concepts introduced in the course to develop an automated verification tool for a language called MicroViper, a subset of the Viper language considered throughout the course. The details of the MicroViper language are specified further below.

We split the task of implementing a MicroViper verifier into core features, which must be implemented by every submission, and extension features, which you should consider implementing if you aim for a good or excellent grade. The individual features are listed further below.

A written report is not required. However, you must add a file README.md that contains the following:

1. Structure of your project, for example the main steps of your toolchain and where each step is found in your code.
2. What has and has not been implemented.
3. How to install and run your project.
4. A brief explanation of your design decisions.
5. An evaluation, for example a set of programs that you verified with both Viper and your implementation.

Grading

As a guideline, your grade is determined by your submission's quality and completeness, that is, how many extension features are supported. Larger groups should aim for supporting more extension features than small groups.

For this project, "supporting a feature" means that the following conditions are met:

1. The feature is implemented and sufficiently documented such that it can be used by other course participants.
2. The README.md justifies why your approach for implementing a feature is sound; if you implement an approach discussed in class, it is OK to refer to the corresponding course material.
3. The feature is tested against at least six (non-trivial) MicroViper programs using the specific feature. Where possible, four of your examples should verify and two should be correctly rejected. The Viper verifier must yield the same result (verify/does not verify) for your test programs unless explicitly stated otherwise in the feature description. You are allowed to use the example programs considered in class.

To obtain the grade 4, your submission must support all core features. An excellent submission aiming for the grade 12 should target four or more extension features.

Programming Language & Infrastructure

Your solution must use an SMT solver, such as Z3, for discharging verification conditions. You can use either an existing Z3 API or generate SMTLIB-2 code and invoke Z3 through your tool.

You can implement your verifier in a programming language of your own choice. For example, there exist libraries for working with Z3 in Rust, F#, and Python.

To reduce the initial overhead, we will provide you with code skeletons including a MicroViper parser and an example for invoking Z3 in selected languages.

Rust code skeleton

F# code skeleton

Every group must submit an original solution. However, it is fine to share supporting infrastructure, for example parsers, as long as you clearly indicate what is shared in your README.md.

Features

We list the core and extension features below. There is no particular order for extension features; you can work on any subset of your choice.

However, remember that you are expected to complete the core features.

You are welcome to propose and implement other extension features. Please first contact the teacher to check if your idea qualifies as an extension feature.

Core Feature 1

Your MicroViper verifier must support programs that consist of a single method, where

• no expression in the method's specification or body uses a division operation (/);
• the method body contains no loops, no method calls, and no user-defined function calls; and
• the method specification contains no user-defined function calls.

Core Feature 2

Your MicroViper verifier must support reasoning about partial correctness (that is, assertion failures still fail verification but termination is not required) of while loops.

Core Feature 3

Your MicroViper verifier must support expressions in the method's specification or body that use the division operation (/).

Hint: Remember to deal with corner cases. For example, what should happen if you add an expression like x / y or 17 / 0 to a pre- or postcondition? Your implementation must remain sound and should be able to verify reasonable usages of /.

Extension Feature 1

Your MicroViper verifier should indicate why verification failed, that is, which specification (e.g. a postcondition) or assertion cannot be verified.

For obvious reasons, supporting this feature does not require that you give example programs that successfully verify.

Extension Feature 2

Extend your MicroViper verifier such that it supports reasoning about partial correctness (that is, assertion failures still fail verification but termination is not required) of multiple methods that may possibly recusively call each other.

Extension Feature 3

Extend your MicroViper verifier such that one can define and call user-defined functions with an implementation, that is an expression that serves as the function body. It is not required that one can attach pre- or postconditions to such functions.

Explain in your README.md whether you use limited functions or not; justify your answer. If possible, try to include examples where using limited functions might help and/or hinder verification.

Hint: Recall that function calls are expressions, that is, they may appear in specifications.

Extension Feature 4

Extend your MicroViper verifier such that one can define and call abstract user-defined functions. That is, it should now be possible to attach pre- or postconditions to user-defined functions; providing a function body is optional.

Hint: Function calls are expressions and may appear in specifications. Consequently, you have to be careful if a function with a pre- or postcondition is called inside of another pre- or postcondition.

Extension Feature 5

Use efficient weakest preconditions in your MicroViper verifier. Try to use larger example programs demonstrating the efficiency gain.

Extension Feature 6

After supporting extension feature 2, extend your MicroViper verifier such that one can declare global variables, that is, var name:type may be used outside of method bodies. For simplicity, we require that global variable names must be distinct from all other variable, method, and function identifiers.

It is not required to compare against Viper for this task.

Hint: Global variables have consequences for how you deal with method calls. You may want to add new annotations to methods. Briefly explain your design decisions in your README.md.

Extension Feature 7

Extend your MicroViper verifier such that one can reason about total correctness of while loops.

It is not required to compare against Viper for this task.

Hint: You may want to add new annotations to loops for checking termination. If you introduce such constructs, briefly explain them in your README.md

Extension Feature 8

Extend your MicroViper verifier such that one can reason about total correctness of recursive methods.

It is not required to compare against Viper for this task.

Hint: You may want to add new annotations to methods for checking termination. If you introduce such constructs, briefly explain them in your README.md

The MicroViper Language

Informal summary

The MicroViper language is a subset of the Viper language with methods, functions, loops, variables of type Int or Bool, variable declarations, assignments, conditionals, and the usual expressions and predicates considered in class. As specification constructs, MicroViper admits assume and assert statements, pre- and postconditions (requires and ensures) as well as loop invariants invariant.

When in doubt, your language should work with the Viper verifier (unless you work on extension features that specifically diverge from Viper). This allows you to test your implementation against Viper.

Language specification

MicroViper programs are given by the grammar below. The grammar uses extended syntax inspired by regular expressions: A* denotes zero or more repetitions of A; A? denotes that A is optional, that is, zero or one appearances of A.

An identifier Ident is any non-empty string that

1. is not a keyword used in the grammar and
2. starts with a letter or _ followed by arbitrary many letters, _ or digits, that is, it is matched by the regular expression [a-zA-Z_][a-zA-Z_0-9]*.

Document ::= DocumentItem*

DocumentItem ::=
    Method |
    Function

Method ::=
    "method" Ident "(" Vars ")"
    "returns" "(" Vars ")")?
    Specification*
    Body?

Function ::=
    "function" Ident "(" Vars ")" ":" Type
    Specification*
    ("{" Expr "}")?

Specification ::=
    "requires" Expr |
    "ensures" Expr

Body ::= "{" Statement* "}"

Statement :=
    "assert" Expr |
    "var" Var (":=" Expr)? |
    "if" "(" Expr ")" Body ("else" Body)? |
    "while" "(" Expr ")" ("invariant" Expr)* Body |
    Idents ":=" Ident "(" Exprs ")" |
    Idents ":=" Expr

Idents ::= Ident | Ident "," Idents

Vars ::= Var | Var "," Vars
Var ::= Ident ":" Type

Type ::= "Int" | "Bool"

Exprs = Expr | Expr "," Exprs
Expr ::=
    "true" |
    "false" |
    "result" |
    Integer |
    Ident |
    "(" Expr ")",
    Ident "(" Exprs ")" |

    "-" Expr |
    "!" Expr |

    Expr "*" Expr |
    Expr "/" Expr |

    Expr "+" Expr |
    Expr "-" Expr |

    Expr "<=" Expr |
    Expr "<" Expr |
    Expr ">=" Expr |
    Expr ">" Expr |
    Expr "==" Expr |
    Expr "!=" Expr |

    "exists" Var "::" Expr |
    "forall" Var "::" Expr |

    Expr "||" Expr |

    Expr "&&" Expr |

    Expr "==>" Expr

We impose a few more rules for MicroViper programs. Your implementation does not have to check them but implementing rudimentary checks (as done by the code skeletons) may help you identifying issues in your test and example programs.

We will only consider MicroViper programs that respect the following rules:

• For each nonterminal, e.g., Expr, rules are grouped together; a newline indicates the beginning of a new group. For example, Expr "*" Expr | Expr "/" Expr is one group and Expr "+" Expr | Expr "-" Expr is another group. The ordering of groups (from top to bottom) indicates the order of precedence. Hence, * and / have a higher precedence than + and -.
• The operators *, /, +, -, &, |, &&, || are left-associative; ; and ==> are right-associative.
• In contrast to the grammar for PL0, we use one nonterminal Expr for all expressions. Still, we only admit well-typed expressions in MicroViper programs, where the admissible types are Int and Bool. For example, if x and y are of type Int, then 17 / x + 3 * y is well-typed, whereas x ==> y + 3 is not. When in doubt, you can use Viper to check whether an expression is well-typed.
• Every expression of type Bool is a predicate. If the expression does not contain any quantifiers (exists or forall), it is a Boolean expression. Predicates may only appear in assert or assume statements as well as in the annotations requires, ensures, and invariant. Boolean expressions can also appear in assignments and as guards of conditionals and loops.
• Variables bound by quantifiers must be distinct from all program variables.
• Identifiers are used correctly (e.g., identifiers representing functions do not appear left of assignments).
• All identifiers representing method and function names must be pairwise distinct from all other identifiers.
• The names of all variables appearing in a method (either as parameters or as locally declared variables) must be pairwise distinct.
• Variables are not allowed to be used before they are declared.
• A method's input parameters (first list Vars in the grammar) are read-only; its output parameters (second list Vars in the grammar) are read-write but have no initial values.
• Output parameters may not appear in a method's precondition.
• Function calls are expressions and can appear in expressions.
• Method calls are statements. They may not appear in expressions. If the list of output parameters of a method is non-empty, then a method call must assign every output parameter to a variable. For example, x, y, z := callMethodWithThreeOutputs().

Project B

This page describes the second project for the verification course, which is concerned with developing verification methodologies. Read the full description carefully. If you need clarification on a task, contact the lecturer.

Deadline: November 30, 23:59

The project can be solved in many different ways. It is essential that you reasonably justify your design decisions.

A written report is not required. However, you must explain your approach and justify your design decisions for each task. We recommend putting your explanations in comments at the beginning of the task's Viper file.

Submission: push your solution to the GitLab repository of your homework group in a directory named project-b. The latest push before the deadline will be considered as your submission.

Files: Viper code skeleton

Tools: All tasks are to be completed using Viper. Your submission must work with the Viper and Z3 versions distributed with the current version of Viper IDE. Your solutions should work with at least one Viper backend (Silicon or Carbon; indicate which one works if it makes a difference).

Background

Throughout the course, we focused on program correctness, that is, how to specify what a program should do and how to verify that it does what has been specified. Apart from writing correct programs, we are also interested in writing efficient programs.

The goal of this project is thus to develop a verification methodology for reasoning about time complexity and to automate that methodology with Viper.

Time complexity

Upper bounds on the time complexity of algorithms are typically described using Big O notation, an abstract that allows us to reason about complexity classes. For example, does a function's runtime grow linearly, quadratically, exponentially, and so on, concerning the function's input size? By using Big O notation, we also abstract from the exact runtime costs of individual instructions (in terms of clock cycles or seconds).

For this project, we will use a simplified notion of time complexity. Instead of using Big O notation, we will assume an abstract time unit and use a runtime model in which every method call and every loop iteration consumes one abstract time unit; all other statements are considered to consume no time at all.

Time units

We considered Viper predicates as a mechanism for abstracting heap-based data structures. In particular, predicate arguments enable abstracting over the content of a data structure. To gain access to and hide the internals of a data structure, we then need to unfold and fold the predicate manually.

In this project, we will use predicates to represent an abstract, non-duplicable resource that does not refer to anything on the heap. Instead, we will use a predicate to indicate one abstract unit of time, called a time credit for short.

predicate time_credit()

Notice that the predicate has neither arguments nor a body. Our runtime model also supplies an abstract method letting time pass by consuming a time credit:

method consume_time_credit()
    requires time_credit()

Whenever a statement consumes time, we invoke the above method to consume a time credit. Intuitively, the number of time credits available to our program thus represents the time that can pass during its execution. Verification will fail if we do not have enough time credits left.

For example, the method below does not verify. In the precondition, we claim that we can execute it with just two time credits, but we consume three time credits in its body:

method example()
    requires time_credit() && time_credit()
{
    consume_time_credit()
    consume_time_credit()
    consume_time_credit() // error: not enough time credits
}

Alternatiely, we can represent the above precondition using fractional permissions, that is, using the following precondition:

    requires acc(time_credit(), 2/1)

Note that unlike heap locations, we can hold more than one full premission to an abstract predicate. This notation also allows us to have arbitrarily many time credits, for example depending on method arguments:

method example2(n: Int)
  requires acc(time_credit(), n/1)

Runtime model

Throughout this project we consider a runtime model that adheres to the following two rules:

1. Every (non-ghost) method implementation must start with a call to consume_time_credit(). Hence, every (executable) method consumes at least one time unit.

2. Every loop body must start with a call to consume_time_credit(). Hence, every loop iteration consumes at least one time unit.

We will not create time credits out of thin air. Instead, the amount of time credits available is determined by the precondition. If we manage to verify a program with these time credits, then the initial amount of time credits is an upper bound on the execution time of a program in our simple runtime model.

More precisely, if time credits are correctly consumed by any operation we use, then we show that the amount of time credits given in the precondition is sufficient to execute a given method. We thus prove an upper bound on the program's execution time with respect to our runtime model.

Note that we could have allocated more time credits in the precondition than required.

Amortized Analysis

Some data structure operations have a costly worst-case execution time but are still very efficient when considering a longer sequence of operations. For example, adding an element to a (dynamically allocated) vector or array is typically constant-time. However, its worst-case execution time may be linear: if we attempt to add an element to a full array, we first need to allocate a larger array and copy over all existing values. Such a worst-case scenario rarely happens since we can add many more elements before reaching the new array's capacity.

Hence, when considering sufficiently many add operations, the average time per method call becomes almost constant. The general technique for analyzing such average time consumption over a sequence of operations is called amortized analysis.

There are multiple approaches to amortized analysis, but the one we will consider is the accounting method (also known as the banker's method). The general idea is that a data structure can store time credits. Operations on the data structure are given a sufficient cost that may also cover extra credit saved in the data structure. Most calls to the method increase the credit balance of the data structure, but the ones that would normally take a longer time consume the stored credit instead.

Task 1: Basic runtime analysis

To get familiar with reasoning about runtimes, we will analyze three methods that we have verified before. In each subtask listed below, you are given an existing method implemented in Viper with a correct functional specification. Find an upper bound of each method’s runtime and specify it using time credits. Try to find the most precise upper bound possible!

1. Analyze the iterative implementation of the Fibonacci numbers in skeleton/task1/fib_iter.vpr.
2. Analyze the recursive implementation of the Fibonacci numbers in skeleton/task1/fib_rec.vpr.
3. Analyze the fast exponentiation algorithm in skeleton/task1/fast_pow.vpr.

Hint: For the third subtask, you may want to prove a logarithmic bound. Instead of defining and using a logarithm function directly, it may be easier to use ghost variables to keep track of the logarithm of some variable. You may also need to introduce lemmas for proving properties of logarithms.

Task 2: Binary search trees

We will consider binary and binary search trees (BSTs) in this task.

A binary tree is a heap-based data structure consisting of nodes containing a value, an optional left subtree, and an optional right subtree.

A binary search tree is a binary tree where all node values in the left subtree are strictly smaller than the current node’s value, and all node values in the right subtree are strictly greater than the current node’s value. Note that this definition also implies that there are no duplicates in the tree.

Modify the file skeleton/task2/trees.vpr when solving the following tasks:

1. Define a binary tree predicate with nodes containing integer values.
2. Define a BST predicate that ensures sortedness of the node values.
3. Implement, specify, and verify a method bst_insert, which takes a value and a BST and inserts the value into the BST, such that the resulting tree remains a BST after the operation.
4. Use the time credit model to prove that the runtime of bst_insert is at most logarithmic in our simple runtime model. To this end, you may want to prove that bst_insert terminates within h+1 time units, where h is the tree's height.

Hints:

• The BST property can be specified without using quantifiers. Consider using abstraction to specify the minimum and maximum values in the given (sub)tree.
• Remember that your implementation of bst_insert must be sufficiently efficient such that you can prove the runtime bound in part 4.

Task 3: Dynamic arrays

In this task, we will consider dynamic arrays, which are arrays that grow as values are inserted. A typical dynamic array has a capacity indicating the number of elements it can store before it needs to be resized. It also has a length indicating the number of elements currently stored. The length is always less than or equal to the capacity.

Modify the file skeleton/task3/dyn_array.vpr when solving the following tasks:

1. Define a predicate for a dynamic array of integers using quantified permissions. Use the provided abstract function array_offset to obtain the heap locations of the array. Use abstraction to define the contents of the array as a sequence.
2. Implement, specify, and verify a naive append method that never resizes the array; this method can thus only be called when there is space for another element.
3. Implement, specify, and verify a method that resizes the array by doubling its capacity. To model reallocation, you can inhale the permissions for the new array, but you should copy the old contents using a loop.
4. Implement, specify, and verify a full append method that calls either of the previous two methods depending on the state of the given dynamic array.
5. Amortized time analysis: Using the time credits stored in the dynamic array predicate, prove that the full append method has an amortized constant runtime.

Task 4: Circular buffers

In this task, we will consider circular buffers and linked lists. Circular buffers are a data structure that uses a fixed size array to implement a FIFO (first in, first out) queue. An offset into the array is maintained as the head, where elements are read from, and another offset defines the tail, where elements are written to. A write operation consists of writing data to the tail offset and incrementing it by one. A read operation consists of reading data from the head offset and incrementing it by one. The buffer is called circular because the offset increments use a modulo operation to wrap around the array's length.

Modify the file skeleton/task4/circular.vpr when solving the following tasks. The skeleton contains an abstract predicate for arrays and a small set of functions and methods for using arrays.

1. Define a circular buffer predicate. Use abstraction to define the contents stored in the circular buffer.
2. Implement, specify, and verify methods to read one element from a circular buffer and to write one element into a circular buffer.
3. Define a predicate for a linked list of integers.
4. Using linked lists, implement, specify, and verify a method to reverse the contents of a circular buffer.