rfc:dbc2

This is an old revision of the document!


PHP RFC: Native DbC support as definition

Important Note

This RFC is a part of “Native DbC support” RFC. http://wiki.php.net/rfc/dbc

There are many way to achieve DbC. This RFC proposes DbC as function/method definition.

Introduction

Design by Contract (DbC) or Contract Programming is powerful program design concept based on Contracts that

  1. Define precondition contract for methods/functions. i.e. Define Parameter value specifications/conditions.
  2. Define postcondition contract for methods/functions. i.e. Define Return value specifications/conditions.
  3. Define invariant contract for methods/functions. i.e. Define class state must be true always.

These contracts are evaluated development time only. Therefore, there is no performance penalty with DbC.

DbC Changes the Way Program is Designed/Developed/Tested

CalleR and CalleE responsibility and validation:
  • With modularized design without DbC, the more code is consolidated, the better code is.
    Therefore, parameter validity is checked deep into the code. Parameter validity check is calleE responsibility.
  • With DbC, parameter checks are done as precondition. Passing valid parameter to a function is calleR responsibility.
Exit value validation:
  • Without native DbC, return value validity cannot be checked without scattered assert() for every place function is used.
    i.e. Programmers has to write “$ret = func(); assert($ret > 0);” everywhere func() is used or code must have assert() for each func().
  • With native DbC, return value validity is checked as postcondition. It does not require scattered assert().
Class state validation:
  • With native DbC, invariant condition may be defined. Invariant allows programmers consolidate class state which must be TRUE for always.
    e.g. $account_balance >= 0

precondition check can be done with assert(), but other feature requires native DbC.

DbC reverses the responsibility caller and callee, ensures parameters, return value and class state validity without performance penalty. This helps PHP to achieve more efficient development by contract errors, faster execution for production.

DbC encourages users to control inputs/output/class state precisely. This helps application efficient/precise development. Languages designed lately have native DbC support. e.g. D language. Almost all languages have some kind of DbC supports today.

Readability of Code / Testing Code

Since contracts are written in function/method definition, it's much easier to find function/method spec compared to conditions written in UnitTests. It also enables contract check for running applications operated by humans.

DbC is NOT a complement of UnitTest, but it provide additional way of testing programs. Programs should be tested by UnitTest with and without DbC. With this procedure, UnitTest condition coverage is improved and/or simplified.

General Concern of Design by Contract

Some may concern that lack of checks under production environment. However, all inputs to programs should validate input parameter validity right after input parameters are passed to program.

This is basic principle of secure programs. Users should not DbC everywhere. User should have proper defense in depth as security measure. Security standard like “ISO 27000” or security guideline like “SANS TOP 25 Monster Mitigations” suggests to have proper output controls, as well as input controls. This applies with or without DbC. DbC encourages proper input/output controls compare to program design without DbC.

Proposal

Introduce native contracts “require”( precondition ), “return”( postcondition ) definition to function/method and special “__invaliant()” method to class.

While new usage of require, return may seem strange at first, users can use familiar PHP syntax for DbC definitions.

  • require(assert-expr [,'Error msg']); Precondition in function/method and invariant in class
  • return(assert-expr [,'Error msg']); Postcondition in function/method. “$>” is used as return value.

require, return behave just like assert().

Example

class Product {
  protected $inventory;
  require($this->$inventory >= 0); // Invariant - Should be always TRUE
 
  // User is supposed to check inventory first
  function haveEnoughInventory($quantity) 
    require($quantity > 0)  // Precondition
  {
    return (bool) ($this->inventory - $quantity) >= 0;
  }
 
  // Sell inventory
  function sell($quantity) 
    require($quantity > 0) // Precondition
    return($> >= 0) // Postcondition. $> is return value
  {
    return $this>inventory - $quantity;
  }
}

Longer Class Definition Example - need better one

class MySession2 extends SessionHandler {
    public $path;
    require(is_string($this->path)) && !empty($this->path));
 
    public function open($path, $name)
        require(strlen($path) > 3 && strlen($name) > 3);
        return(is_bool($>));
    {
        if (!$path) {
            $path = sys_get_temp_dir();
        }
        $this->path = $path . '/u_sess_' . $name;
        return true;
    }
 
    public function close()
        return(is_bool($>))
    {
        return true;
    }
 
    public function read($id) 
        return(is_string($>) && strlen($id) > 10)
    {
        return @file_get_contents($this->path . $id);
    }
 
    public function write($id, $data) 
        require(strlen($id) > 10 && strlen($data) > 10)
        return(is_bool($>));
    {
        return file_put_contents($this->path . $id, $data);
    }
 
    public function destroy($id) 
        require(strlen($id) > 10)
        return(is_bool($>))
    {
        @unlink($this->path . $id);
    }
 
    public function gc($maxlifetime) 
        require($maxfiletime > 60)
        return($> > -1) // GC supposed to return number of deleted records. Code is wrong
    {
        foreach (glob($this->path . '*') as $filename) {
            if (filemtime($filename) + $maxlifetime < time()) {
                @unlink($filename);
            }
        }
        return true;
    }
}

Execution Control

Introduce “dbc” INI switch, Off by default. No additional CLI option for DbC.

A method/function is executed as follows

Basic Execution

require() - executed before function body return() - executed upon return invariant - executed after require() and before return(). There are few exceptions explained later.

Development mode: dbc=On
  1. require() conditions
  2. class invariant
  3. method()
  4. class invariant
  5. return() conditions
Production mode: dbc=Off
  1. method()
Execution details when DbC is enabled

Invariant and Special Methods

  • __constructs()/__wakeup()/__set_state() will NOT execute invariant on entry.
  • __destruct()/__sleep() will NOT execute invariant on exit

Class Inheritance

  • When parent class methods are called, DbC conditions are executed
  • Special methods execution exception is the same

Abstract Class

  • The same as usual class.

Trait

  • The same as usual class.

Static Call

  • Only pre/post contracts are executed

Interface

  • Cannot define DbC contracts.

Backward Incompatible Changes

None

  • No additional keyword

Proposed PHP Version(s)

  • PHP7

RFC Impact

To SAPIs

None

To Existing Extensions

None

To Opcache

Dmitry, could you write impact when discussion is finished?

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

  • 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.1423551602.txt.gz · Last modified: 2017/09/22 13:28 (external edit)