Home

Design By Contract (DbC) is a software correctness methodology. It uses preconditions and postconditions to document (or programmatically assert) the change in state caused by a piece of a program.

Attributes of Design by Contract philosophy

Classes should specify their invariants: what is true before and after executing any public method. Methods should specify their pre- and post-conditions: what must be true before and what must be true after their execution, respectively. Pre-conditions may be weakened by subclasses and post-conditions may be strengthened. The explicit definition of these "assertions" forces the designer to think deeply about what is a requirement of the specification and what is an artifact of a particular implementation. These assertions can and should influence the declaration of "throws" exceptions as well as the throwing of runtime exceptions and try/catch in general. For example if a method has specified some pre-condition then the failure of that condition is the responsibility of the client of the method. The method should not have to declare a checked exception for that condition, it should not have to test and throw for that condition, and likewise the client should not have to try/catch for that condition. The client should do whatever is necessary to ensure it will meet the pre-conditions. It may do runtime tests or it may assume some condition is satisfied based on its own specification.

Performance implications

Contract conditions should never be violated during execution of a bug-free program. Contracts are therefore typically only checked in debug mode during software development. Later at production, the contract checks are disabled to maximize performance. This technique is implemented now with Aspect-Oriented Paradigm provided by Go! AOP framework by adding an aspects that checks extra-condition only for development mode.

Framework configuration and installation

Framework can be installed via composer. As this tool is mainly designed for development mode, suggest way to install it is by executing a composer require-dev command:

composer require --dev lisachenko/php-deal

After that you will get the latest stable version of framework. Next step is to configure the framework by specifying directory for cache. For additional information, see example from AOP configuration page.

Configuration is made with simple PHP code:

use PhpDeal\ContractApplication;

ContractApplication::getInstance()->init(array(
    'debug'    => true,
    'appDir'   => __DIR__,
    'cacheDir' => __DIR__.'/cache/',
));

Recommended way to include this file is to add it in the boostrap file of your application or framework right after the composer:

// load composer
include __DIR__.'/../vendor/autoload.php';

if (IS_DEVELOPMENT_MODE) { // change this line for you app
    // initialize DbC framework
    include_once __DIR__.'/dbc_bootstrap.php';
}

Remember, that framework is installed with --dev option. This means that it won't be installed for production mode and there can be an error about missing classes. If you know what you are doing, then you can add the framework without --dev option.

Defining pre-conditions

Preconditions are conditions that must be true prior to running a method. Each method will have its own precondition. These conditions can apply to one of two things: data members or parameters. Typically, they apply to parameters. For example, you might have an Account object and a deposit() method. The deposit() method would, presumably, take an argument indicating the amount of money to be deposited, and that money should be positive. So, a precondition would be amount of money > 0.

Pre-condition for method can be defined with PhpDeal\Annotation\Verify doctrine annotation in the method docblock. To add this annotation marker into the current class, import it via use PhpDeal\Annotation as Contract and then add a block into method:

namespace Demo;

use PhpDeal\Annotation as Contract;

class Account
{
    protected $balance = 0.0;

    /**
     * Deposits fixed amount of money to the account
     *
     * @param float $amount
     *
     * @Contract\Verify("$amount>0 && is_numeric($amount)")
     */
    public function deposit($amount)
    {
        $this->balance += $amount;
    }
}

All pre-conditions will be checked then before the execution of original method body. You can add as many pre-conditions, as you want. So, if you try then to invoke a method Demo\Account->deposit(-100) it will raise an exception because pre-condition asserts that $amount parameter should be always greater than zero.

Defining post-conditions

Where preconditions serve to let the caller of a method know when it's safe to call a method, post-conditions let the caller of a method know what happens after the method has completed calling. Usually, post-conditions are harder to specify. The purpose of a post-condition is threefold:

• to indicate how the data members have changed
• to indicate how the parameters passed in have changed
• to indicate what the value of the return type is In a nutshell, the post-conditions tell you what happened after calling the method. The reason it's difficult to specify a post-condition is that it can be difficult to describe the underlying data structure.

Post-condition is called an "ensure" contract in terms of DbC, so this check can be added with PhpDeal\Annotation\Ensure doctrine annotation class. To define a condition, just add this annotations with valid PHP expression to the method doc-block as following:

namespace Demo;

use PhpDeal\Annotation as Contract;

class Account
{
    protected $balance = 0.0;

    /**
     * Deposits fixed amount of money to the account
     *
     * @param float $amount
     *
     * @Contract\Ensure("$this->balance == $__old->balance+$amount")
     */
    public function deposit($amount)
    {
        $this->balance += $amount;
    }
}

Here we define a safety-check, that our method is really do it's job and if something went wrong, then exception will be raised.

Defining invariant for a class

A class invariant is a property that each instance of the class is guaranteed to have when a method is called (like a common pre-condition for all methods), and that in return each method and constructor must ensure remains true when they terminate (like a common post-condition).

They are good for expressing consistency conditions. An Account class that modelizes an actual wallet might have the class invariant that the amount of money is always positive.

Invariant can be declared only for class via PhpDeal\Annotation\Invariant annotation:

namespace Demo;

use PhpDeal\Annotation as Contract;

/**
 * Simple trade account class
 * @Contract\Invariant("$this->balance > 0")
 */
class Account
{

    /**
     * Current balance
     *
     * @var float
     */
    protected $balance = 0.0;
}

Invariant is checked before execution of every public method and after the execution of every public method.

Expression syntax

PhpDeal uses native PHP expression syntax to work with assertions in conditions. Each parameter of function can be accessed via variable with the same name:

    /**
     * Deposits fixed amount of money to the account
     *
     * @param float $amount
     *
     * @Contract\Verify("$amount>0 && is_numeric($amount)")
     */
    public function deposit($amount);

To access a current object, just use $this magic variable, available for dynamic methods. For post-conditions and cloneable objects, there is a special variable, called $__old which equals to the state of $this before execution of method. This can be useful for state checks:

    /**
     * Deposits fixed amount of money to the account
     *
     * @Contract\Ensure("$this->balance == $__old->balance+$amount")
     */
    public function deposit($amount)
    {
        $this->balance += $amount;
    }

There is one more special variable, available for post-conditions, called a $__result which holds a return value from method:

    /**
     * Returns current balance
     *
     * @Contract\Ensure("$__result == $this->balance")
     * @return float
     */
    public function getBalance()
    {
        return $this->balance;
    }