-
Notifications
You must be signed in to change notification settings - Fork 1
Demo Walk Throughs
This page walks through the process of generating contracts for the sample projects bundled with Celeriac.
This walk-through provides an example of using Celeriac and Daikon to generate Code Contracts for a project. The Bank Account project consists of two parts: (1) an account interface with methods for deposits, transfers, and withdrawals, and (2) a account class with a minimum balance. Additionally, the solution includes an NUnit project to test the basic functionality of the account class.
Open the BankAccount solution in Visual Studio and perform a Debug build of the solution. The test project uses NUnit, so you may need to install NUnit from the Visual Studio package manager.
Since the project uses NUnit, we'll use Celeriac in offline mode. First we'll instrument BankAccount.dll, and then run the NUnit tests in BankAccount.Tests.dll. Since we're generating a trace from the tests, we'll be instrumenting the BankAccount.dll in the output directory of the testing project: BankAccount.Tests\bin\Debug.
A purity file adds extra "fields", which are really method calls to a given type, to Celeriac's output. Pure methods are methods which have no external side effects, for example get properties, ToString(), and other observer methods. Any zero-parameter method, or method whose only parameter is the type of the receiver, can be added as a pure method. First, we'll have Celeriac list all of the nullary (methods not taking an argument) that could possible appear in the purity file.
CeleriacLauncher.exe --emit-nullary-info .\BankAccount.dll
This will create the file BankAccount_auto.pure. If you open the file, you will see that it lists methods for
application types such as BankAccount and IAccount, as well as system types such as System.Reflection.MethodBase and System.String. You'll want to remove the lines that correspond to (1) methods at the modify state, and (2) methods you aren't interested in. Note that property getters have the name get_Property. For this example, we'll just keep our application-specific methods:
BankAccount.BankAccount, BankAccount, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null;get_Balance
BankAccount.BankAccount, BankAccount, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null;get_IsActive
BankAccount.BankAccount, BankAccount, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null;get_MinimumBalance
BankAccount.IAccount, BankAccount, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null;get_Balance
BankAccount.IAccount, BankAccount, Version=1.0.0.0, Culture=neutral, PublicKeyToken=null;get_IsActive
and save the file as BankAccount.pure. We leave off the IAccountContracts methods since they're for the contract class where we'll place Code Contracts for the IAccount interface.
Notice that some of the methods, such as get_Balance, appear to be listed twice: once for BankAccount and once for IAccount. Each line in the purity lists a method to be called when the declared type of an expression corresponds to the type of the line. Therefore, if an expression is an IAccount, only the values methods included for IAccount will be output, even if the runtime type of the expression is BankAccount or another account type with additional methods (i.e., the minimum balance will not be recorded).
The next step is to instrument the assembly, passing in the purity information. The enhanced version of Daikon we maintain supports additional flags to ensure the proper display of invariants for .NET programs and the filter of uninteresting contracts. Include the --is_property_flags and --is_readonly_flags options to enable these features.
CeleriacLauncher.exe --is_property_flags --is_readonly_flags --purity-file=BankAccount.pure --save-program=BankAccount.dll.instr BankAccount.dll
This will create a metadata file daikon-output\BankAccount.decls and an instrumented assembly BankAccount.dll.instr. Next, replace the original DLL with the new, instrumented DLL:
mv BankAccount.dll BankAccount.dll.orig
mv BankAccount.dll.instr BankAccount.dll
To run the test suite, open BankAccount.Tests.dll in the NUnit GUI and then run the tests as usual (or use the command line runner). This will create a file daikon-output\BankAccount.test-domain-BankAccount.Tests.dll.dtrace.
If you look at the generated trace, you'll see that it contains a section for each method entry and exit; with the first entry being a constructor call to BankAccount:
BankAccount.BankAccount..ctor(System.Decimal\_minimumBalance,\_System.Decimal\_initialBalance):::ENTER
this_invocation_nonce
2
minimumBalance
0
1
System.Decimal.MaxValue
79228162514264337593543950335
1
System.Decimal.MinusOne
-1
1
System.Decimal.MinValue
-79228162514264337593543950335
1
System.Decimal.One
1
1
System.Decimal.Zero
0
1
initialBalance
0
1
By default, Celeriac will output subexpression values up to a depth of two. Therefore, we see entries for System.Decimal.MaxValue, etc. since the parameters to the constructor have declared type decimal. We don't see entries for fields and pure methods of the account though, since this trace is for the entry to the constructor call.
To generate Code Contracts from the test suite trace, we'll use Daikon with the csharpcontract format specified (remember to change the command to reflect your Daikon JAR location):
java -cp C:\lib\daikon\daikon.jar daikon.Daikon --format csharpcontract .\daikon-output\BankAccount.decls .\daikon-output
\BankAccount.test-domain-BankAccount.Tests.dll.dtrace
This will output the inferred Code Contracts for each program point. For example, the inferred object invariants for the BankAccount class are:
BankAccount.BankAccount:::OBJECT
this.balance == this.Balance
this.minimumBalance == this.MinimumBalance
this.balance >= 0.0
this.minimumBalance.OneOf(0.0, 10.0, 50.0)
this.GetType() == typeof(BankAccount.BankAccount)
this.Balance >= 0.0
this.MinimumBalance.OneOf(0.0, 10.0, 50.0)
this.balance >= this.minimumBalance
this.balance >= this.MinimumBalance
this.minimumBalance <= this.Balance
this.Balance >= this.MinimumBalance
These contracts are pretty straight-forward: they capture they important fact that the account balance must be greater than the minimum balance, as well as relating the properties to their backing fields.
However, the contract this.MinimumBalance.OneOf(0.0, 10.0, 50.0) is clearly invalid: the contract is true with respect to the tests we ran, but it doesn't capture the real behavior of the program. By default, Daikon will not generalize to inequalities until after it has seen more than three different values for an expression. Therefore, to generate better invariants, we need to either write test cases that set more than 3 different minimum balances, or override Daikon's default.
To produce more readable contracts, some contracts in the C# Code Contract format make use of utility extension methods. The OneOf method in the above contracts is an example of one such method.
In the Code Contract system, methods that implement an interface or override a method cannot specify additional preconditions (Contract.Requires statements). However, the method can promise additional facts/postconditions. Therefore, contracts are generated for the entry points of IAccount's methods, but not for the corresponding implementations in BankAccount.
The contracts inferred for interfaces such as IAccount must hold true for all implementing methods. For the provided test suite, the following contracts are inferred. As before, the contracts destination.Balance == 250.0 and amount == 100.0 suggest that tests should be created to cover more values.
BankAccount.IAccount.TransferFunds(BankAccount.IAccount destination, System.Decimal amount):::ENTER
destination != null
destination.GetType() == typeof(BankAccount.BankAccount)
destination.Balance == 250.0
destination.IsActive == true
amount == 100.0