Provable Code

Tools and patterns for using mathematics to write more reliable and readable software
Course info
Rating
(92)
Level
Intermediate
Updated
Jun 13, 2012
Duration
5h 51m
Table of contents
Description
Course info
Rating
(92)
Level
Intermediate
Updated
Jun 13, 2012
Duration
5h 51m
Description

Bertrand Meyer defined Design by Contract as a system of documenting and proving the responsibilities of a software system. Today, we have tools built into our compilers and type systems that help us to prove those assertions. This course will introduce you to some of those tools, define systems of logic for reasoning about code, and recommend patterns for building provable software.

About the author
About the author

Mathematician and software developer, Michael L Perry applies formal proof to creating reliable software. He has developed a method starting from the works of the greats (Meyer, Rumbaugh, Knuth), and embodied it in his open-source frameworks (Update Controls and Correspondence).

More from the author
Entity Framework Migrations for Large Teams
Intermediate
1h 51m
Aug 16, 2016
More courses by Michael Perry
Section Introduction Transcripts
Section Introduction Transcripts

Design by Contract
Bertrand Meyer wrote an industry changing book in 1997 called "Object Oriented Software Construction. " In it he introduced the idea of design by contract. Which applies the rules of predicate calculus and first order logic to software correctness. He also introduced the language Eiffel, the first programming language to include correctness assertions in the form of predicates as first class constructs. In this module we will study Bertrand Meyer's design by contract. We'll start by examining some typical source code and determining what assertions we can make about it. Then we will introduce the concept of preconditions. Assertions that must be proven before the code can be executed. Then we'll look at post condition and class in variance. These are assertions that a class promises will be true after it completes its work. We'll examine the strength of assertions and decide when they should be strong or weak. And then we'll take a look at inheritance to determine what impact it has on the strength of class assertions. Finally we'll discuss what software correctness really means and try to determine what tools we need to make it feasible.

Code Contracts
In this module we're going to examine code contracts. Code Contracts is a tool from Microsoft research that integrates with Visual Studio in order to prove the correctness of our code. It includes a class library that gives us runtime contract checking and a compiler plugin that gives us static contract checking. So to get started, you want to go to research. microsoft. com/contracts and download Code Contracts and the documentation. Go ahead and save the documentation for later reference. And then you'll want to go into Visual Studio's extension manager and get the Code Contracts editor extensions. Once you've done that, then you can go into your project properties and you can enable perform runtime contract checking and perform static contract checking. And then within your code you use the contract class to specify your assertions, preconditions, using the requires method, postconditions using ensures, and invariance using the invariant method.

Degrees of Freedom
Welcome back to the 5th module of Provable Code. In this module we're going to be talking about degrees of freedom. This is a mathematical concept that tells you how flexible a system is. How many orthogonal dimensions can the system move in at the same time and this is going to be a very important piece of analysis that will help us to prove the correctness of our code that it matches a specific system that we're trying to model. So the things that we're going to talk about with degrees of freedom is first of all we're going to look at a figure in a plane. Now we're going to see how that figure represents degrees of freedom on a two dimensional surface. And then we're going to examine a system of equations and count the unknowns in the equations in that system and by doing so that will help us to count the degrees of freedom in that system. And then we will examine some patterns for representing degrees of freedom in code and for keeping other parts of the system in sync within the system that we are trying to model. And then we are going to prove that our code satisfies the system that we are modeling based on those patterns that we're using.

Immutability
Welcome back to the sixth and final module of Provable Code. This module is about immutability. And we're going to use this topic of immutabilities to sort of wrap it all up, put a nice bow in it and bring everything that we've learned together. So, in this module we're going to be talking about the assignment statement in C#. And take a look at specifically how assignments make proof a little bit more difficult than they need to be. And from there, we'll examine why functional languages tend to be developed the way they are so that they eliminate assignment statements. And then we'll see how we can use functional languages like F# to make our C# code more approvable. And then bring it back to C# we're going to revisit the constructors and see how this pattern in addition to being able to prove that something is done once and only once. And before anything else, we can see how constructors factor into immutability. And then we're going to take a look at the different categories of state. And from that derive different categories of classes. And after we've constructed a system suing the various categories of classes, then we'll take a look at a pattern using dependency chains in order to prove the things have happened in the right order.