Updates:
Part 4: Object Ownership/Assertions & Assumptions
Part 5: Frame Conditions/Inheritance/Boogie
Part 6: Implementing a non-null string collection
Part7: Spec# Wrapup
In my previous posts regarding
Spec#, I have discussed some of the general concepts. Let's review each one before we move onto today's topic, because each one builds upon another.
Part 1: Spec# introduction
Part 2: Method Contracts (Preconditions/Postconditions)
Now that we're caught up, let's move on. Today's topic is going to look at
Invariants. On the first post, I mentioned that
Design by Contract we have three parts.
They are as follows:
- What do we expect?
- What do we guarantee?
- What do we maintain?
Now that we covered the first two with preconditions and postconditions, it's time to move onto "What do we maintain?" and that's where invariants come into play.
Invariants are somewhat similar to postconditions in that they ensure that your code is correct when it returns. They are used in the context of a class and specify what conditions must hold throughout the classes lifetime. They refer to class methods and private fields, but not part of the public interface. We'll talk about two types of them, the class invariant and the loop inviariant.
The invariants are specified in Spec# by the invariant keyword.
Class Invariants
When using
class invariants, Spec# adds a boolean field called
inv to classes which tells the runtime whether the invariant currently holds. If it does hold, then the object is said to be in a consistent state. While the
inv field is true, the fields within the object cannot be modified due to the possibility of breaking any of the invariants.
If you need to update any of the invariant fields, Spec# makes you expose the object inside of an
expose block. At the beginning of the
expose block, the
inv field is set to false, and at the end it is checked. If the invariant still holds, then the
inv field is set to true again, else an exception is thrown and you were indeed a naughty programmer. You cannot also add a return statement inside of an expose block, nor can you call any method that requires a consistent state. The runtime system makes sure that the object is always in a consistent state and the invariants hold.
Let's look at a simple invariant class. Let's start with a simple Date class:
public class Date
{
int day;
int month;
int year;
invariant day >= 1 && day <= 31;
invariant month >= 1 && month <= 12;
invariant year >= 1;
public Date()
{
// Fields must be initialized in the constructor
day = 14;
month = 12;
year = 2007;
}
}
As you can note from the above class, I specified that the day cannot be less than 1 nor greater than 31, the month cannot be less than 1 nor greater than 12 and the year must be greater than 0. We must initialize our fields inside of the constructor in order for this to be valid. Now let's move onto another sample which includes the expose block.
public class Date
{
int daysLeft;
int daysPassed;
invariant daysLeft + daysPassed == 365;
public Date()
{
// Fields must be initialized in the constructor
daysLeft = 16;
daysPassed = 349;
}
public void AddOneDay()
{
expose(
this)
{
daysLeft--;
daysPassed++;
}
}
}
Since incrementing the daysPassed and decrementing the daysLeft would break the invariant, we had to expose it so that it can be checked. At the end, the runtime checks to see that sure enough, we haven't broken the invariant.
Loop Invariants
The second type of invariant I'll cover today is the loop invariant. This invariant specifies conditions that must hold during the execution of a loop. One important note is that these loop invariants are checked before the loop conditions are checked. The loop condition itself cannot be an invariant due to the last iteration of the loop must return false and that would break an invariant.
Now let's walk through a code example of something using a loop invariant. This code will take in an array of 32-bit integers and add them together and return the sum. The code should look like this:
public static int SumAllNumbers(
int[]! numArray)
ensures result ==
sum{
int i
in (0: numArray.Length); numArray[i]};
{
int sumValue = 0;
for (
int idx = 0; idx < numArray.Length; idx++)
invariant idx <= numArray.Length;
invariant sumValue == sum{
int i
in (0: idx); numArray[i]};
{
sumValue += numArray[idx];
}
return sumValue;
}
From the above code, we have a function called SumAllNumbers. We must pass in a non-null array of 32-bit integers, and the postcondition states that the result must be the sum of all numbers. We are using a built-in function call
sum in the postcondition to ensure the numbers add up. There are many of these built-in functions such as
count,
product,
forall and so on. There is a lot to learn and not much documentation to learn by, so that's why I'm bringing this material to you. But, let's continue with the code.
As you will note, we specify a loop invariant for the idx to make sure we do not go outside the bounds of the incoming numArray. We also specify a loop invariant to specify that the sumValue will be the sum of all numbers by using the built-in
sum function.
Wrapup
We learned quite a bit about invariants, and really, we only scratched the surface of what they can do and what they are used for. Most of these concepts are taught in many CS courses, or at least should be. We still have a lot to go!
Upcoming posts to include:
- Object Ownership
- Assertions
- Spec# Attributes
- Boogie static verifier
- And much much more!
So, stay tuned. Develop, mentor and inspire!
