rfc:dbc2
Differences
This shows you the differences between two versions of the page.
Both sides previous revisionPrevious revisionNext revision | Previous revisionNext revisionBoth sides next revision | ||
rfc:dbc2 [2015/02/10 11:49] – dmitry | rfc:dbc2 [2015/02/10 21:44] – typo yohgaki | ||
---|---|---|---|
Line 6: | Line 6: | ||
* First Published at: http:// | * First Published at: http:// | ||
- | ===== Important Note==== | + | ===== Important Note ===== |
This RFC is an alternative approach to " | This RFC is an alternative approach to " | ||
http:// | http:// | ||
- | This RFC proposes PHP syntax extension for contracts declaration. | + | Contracts can be defined without modification to the language, however, the D documentation calls the resulting implementation " |
- | ===== Introduction ===== | + | Other advantages of a native implementation, |
- | Design by Contract (DbC) or Contract Programming is powerful program design concept based on **Contracts** that | + | |
+ | | ||
+ | | ||
+ | | ||
+ | * handling of contract inheritance | ||
- | - Define **precondition** contract for methods/ | + | All of the above applies to PHP. |
- | - Define **postcondition** contract for methods/ | + | |
- | - Define **invariant** contract for methods/ | + | |
- | These contracts are evaluated at run-time, usually durunf development and testing only. It should be possible to switch off contracts validation for production. | + | ===== Introduction ===== |
- | * http:// | + | The D manual contains the following succinct definition of contracts: |
- | * http:// | + | |
- | ====DbC Changes | + | > The idea of a contract is simple - it's just an expression that must evaluate to true. If it does not, the contract |
- | ==CalleR and CalleE responsibility and validation: | + | This should be easily comprehensible, it further validates |
- | * With modularized design without DbC, the more code is consolidated, | + | |
- | * With DbC, parameter checks are done as **precondition**. Passing valid parameter to a function is __calleR__ responsibility. | + | |
- | ==Exit value validation:== | + | ===== Proposal ===== |
- | * Without native DbC, return value validity cannot be checked without scattered assert() for every place function is used. \\ i.e. Programmers has to write " | + | |
- | * With native DbC, return value validity is checked as **postcondition**. It does not require scattered assert(). | + | |
- | ==Class state validation:== | + | Support for the following contracts will be introduced: |
- | * 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** | + | * precondition |
- | + | * postcondition | |
- | DbC reverses the responsibility caller and callee, ensures parameters, | + | * invariant |
- | + | ||
- | DbC encourages users to control inputs/ | + | |
- | + | ||
- | ====Readability of Code / Testing Code==== | + | |
- | + | ||
- | Since contracts are declared together with function/ | + | |
- | + | ||
- | 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" | + | |
- | + | ||
- | + | ||
- | ===== Proposal ===== | + | |
- | We are going to introduce native PHP syntax for contracts declaration for functions | + | ===== Pre and Post Condition ===== |
- | * " | + | These contracts should be defined after the function declaration, but before the function body. |
- | * " | + | |
- | These contracts | + | Multiple precondition and postcondition |
< | < | ||
Line 91: | Line 68: | ||
</ | </ | ||
- | Invariant contracts | + | ===== Invariant ===== |
+ | |||
+ | Invariant contracts | ||
< | < | ||
Line 123: | Line 102: | ||
</ | </ | ||
- | Invariant contracts are not validated | + | **Invariant contracts are not evaluated |
====Contracts Inheritance Rules==== | ====Contracts Inheritance Rules==== | ||
- | **TODO** | + | |
+ | Contracts are constant, this has the following implications: | ||
+ | |||
+ | | ||
+ | | ||
+ | |||
+ | Thus, given the following code: | ||
+ | |||
+ | < | ||
+ | class Child { | ||
+ | require ($this-> | ||
+ | |||
+ | public function someMethod($input) | ||
+ | require(somethingAbout($input)) { | ||
+ | /* ... */ | ||
+ | } | ||
+ | |||
+ | /* ... */ | ||
+ | } | ||
+ | |||
+ | class Monster extends Child { | ||
+ | require ($this-> | ||
+ | |||
+ | public function someMethod($input) | ||
+ | require(somethingElseAbout($input)) { | ||
+ | /* ... */ | ||
+ | } | ||
+ | |||
+ | /* ... */ | ||
+ | } | ||
+ | </ | ||
+ | |||
+ | //Monster// must not break **any** contract in //Child//. | ||
====Execution Control==== | ====Execution Control==== | ||
Line 136: | Line 147: | ||
* 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(). | * 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 if " | + | The default value is " |
- | ===Contracts | + | ===Contracts |
If " | If " | ||
- | - all require() contracts (preconditions) defined for this methods | + | - all require() contracts (precondition) defined for this function |
- | - all require() contracts (invariants) defined | + | - all require() contracts (invariant) for this class and parents |
- method body | - method body | ||
- | - all require() contracts (invariants) defined | + | - all require() contracts (invariant) for this class and parents |
- | - all return() contracts (postconditions) defined for this methods | + | - all return() contracts (postcondition) defined for this function |
**Invariant and Special Methods** | **Invariant and Special Methods** | ||
Line 152: | Line 163: | ||
* < | * < | ||
* < | * < | ||
- | |||
- | **Class Inheritance** | ||
- | |||
- | * When parent class methods are called, DbC conditions are executed | ||
- | * Special methods execution exception is the same | ||
**Static Call** | **Static Call** | ||
- | * Only pre/post contracts | + | * Only pre and post conditions |
- | + | ||
- | **Interface** | + | |
- | + | ||
- | * Cannot define DbC contracts. | + | |
===== Backward Incompatible Changes ===== | ===== Backward Incompatible Changes ===== | ||
Line 236: | Line 238: | ||
===== Rejected Features ===== | ===== Rejected Features ===== | ||
Keep this updated with features that were discussed on the mail lists. | Keep this updated with features that were discussed on the mail lists. | ||
- |
rfc/dbc2.txt · Last modified: 2018/03/01 23:19 by carusogabriel