rfc:dbc2

PHP RFC: Native DbC support as definition

Important Note

This RFC is part of “Design by Contract Introduction” RFC

This RFC is an alternative approach to “Native DbC support” RFC.

Contracts can be defined without modification to the language, however, the D documentation calls the resulting implementation “clumsy and inconsistent”.

Other advantages of a native implementation, also taken from the D manual:

  • a consistent look and feel for the contracts
  • tool support
  • compiler optimizations
  • easier management and enforcement of contracts
  • handling of contract inheritance

All of the above applies to PHP.

Introduction

The D manual contains the following succinct definition of contracts:

The idea of a contract is simple - it's just an expression that must evaluate to true. If it does not, the contract is broken, and by definition, the program has a bug in it. Contracts form part of the specification for a program, moving it from the documentation to the code itself. And as every programmer knows, documentation tends to be incomplete, out of date, wrong, or non-existent. Moving the contracts into the code makes them verifiable against the program.

This should be easily comprehensible, it further validates the argument that the best implementation is a native one, so that the programmer really can “move the specification from the documentation to the code”.

Proposal

Support for the following contracts will be introduced:

  • precondition “require”( precondition-expression [,'Error msg'])
  • postcondition “return”( return_value, postcondition-expression [,'Error msg'])
  • invariant “require”( invariant-expression [,'Error msg'])

Pre and Post Condition

These contracts should be defined after the function declaration, but before the function body.

Multiple precondition and postcondition contracts may be used. The expressions are just a regular PHP expressions. They are evaluated in the function scope, and can access arguments and other scope variables, and return value (via a reserved name). Pre and post-conditions can't be defined for abstract methods and methods defined in interfaces.

function add(int $a, int $b) : int
	require($a > 0)
	require($b > 0)
	return($ret, $ret > 0, "something wrong")
{
	return $a + $b;
}

this code is going to be evaluated as

function add(int $a, int $b) : int
{
	assert($a > 0);
	assert($b > 0);
	$ret = $a + $b;
	assert($ret > 0, "something wrong");
	return $ret;
}

Invariant

Invariant contracts are declared using require inside class body. Multiple invariant contracts may be used. They may access object or static properties through $this and self. Invariant contracts may be used for classes, abstract classes and traits, but not for interfaces.

class Accumulator {
	private $sum = 0;
	
	function add(int $a)
		require($a > 0)
	{
		$this->sum += $a;
	}

	require($this->sum > 0, "overflow detected");
}

this code is going to be evaluated as

class Accumulator {
	private $sum = 0;
	
	function add(int $a)
	{
		assert($a > 0);
		assert($this->sum > 0, "overflow detected");
		$this->sum += $a;
		assert($this->sum > 0, "overflow detected");
	}
}

Invariant contracts are not evaluated when object properties are changed from outside the class scope.

Contracts Inheritance Rules

Contracts are constant, this has the following implications:

  • a derived class must satisfy invariant contracts of it's parent
  • a derived class overriding a method must satisfy the pre and post condition contracts of it's prototype.

Thus, given the following code:

class Child {
    require ($this->age < 18);
    
    public function someMethod($input) 
        require(somethingAbout($input)) {
        /* ... */
    }

    /* ... */
}

class Monster extends Child {
    require ($this->odour == OBNOXIOUS);

    public function someMethod($input) 
        require(somethingElseAbout($input)) {
        /* ... */
    }

    /* ... */
}

Monster must not break any contract in Child.

Execution Control

A new “dbc” INI switch is going to be introduced. It may get the following values:

  • dbc=on - generate code for contracts and check them at run-time. Program, at any time, may change this settion to dbc=off through ini_set().
  • dbc=off - generate code for contracts but don't check them at run-time. Program, at any time, may change this settion to dbc=on through ini_set().
  • dbc=zero_cost - don't generate code for contracts. This may be set only in php.ini and can't be changed through ini_set().
The default value is "off".

Contracts Execution Order

If “dbc” is set to “on”, the order of contracts validation is the following:

  1. all require() contracts (precondition) defined for this function (and prototype where applicable)
  2. all require() contracts (invariant) for this class and parents
  3. method body
  4. all require() contracts (invariant) for this class and parents
  5. all return() contracts (postcondition) defined for this function (and prototype where applicable)

Invariant and Special Methods

  • __constructs()/__wakeup()/__set_state() will NOT execute invariant before method body.
  • __destruct()/__sleep() will NOT execute invariant after method body.

Static Call

  • Only pre and post conditions are executed.

Backward Incompatible Changes

None

  • No additional keyword

Proposed PHP Version(s)

  • PHP7

RFC Impact

To SAPIs

None

To Existing Extensions

None

To Opcache

Opcache will have to be extended to support contracts and store them in shared memory.

New Constants

None

php.ini Defaults

dbc=Off for all (INI_ALL)

  • hardcoded default values
  • php.ini-development values
  • php.ini-production values

Open Issues

  • Contracts inheritance rules
  • Consider introduction of static require() as class invariant for static methods
  • Need to discuss syntax
  • How to manage votes for 2 RFCs

Unaffected PHP Functionality

This RFC does not affect any existing features

Future Scope

Documentation systems may adopt native DbC syntax for documentation purpose.

Vote

This project requires a 2/3 majority

  • Option would be YES/NO only

Patches and Tests

Links to any external patches and tests go here.

If there is no patch, make it clear who will create a patch, or whether a volunteer to help with implementation is needed.

Make it clear if the patch is intended to be the final patch, or is just a prototype.

Implementation

After the project is implemented, this section should contain

  1. the version(s) it was merged to
  2. a link to the git commit(s)
  3. a link to the PHP manual entry for the feature

References

Rejected Features

Keep this updated with features that were discussed on the mail lists.

rfc/dbc2.txt · Last modified: 2017/09/22 13:28 (external edit)