README

Contracts for PHP，是一个用于PHP的合同编程框架和测试工具，它使用属性来提供运行时检查。（特别是，这不是一个静态分析工具。）

内容

• 需求
• 安装
• 配置
• 用法
  • 不变量
  • 方法合同
• 特性

需求

• PHP 8.1+

安装

该库作为composer仓库提供，可以在项目根目录中通过以下命令安装。

$ composer require serafim/dbc

配置

默认情况下，合同的行为取决于系统上是否启用了断言（php.ini配置中的assert.active）。

但是，您可以强制启用或禁用合同

use Serafim\Contracts\Runtime;

// Enable runtime contract assertions
Runtime::enable();

// Disable runtime contract assertions
Runtime::disable();

// Enable runtime contract assertions if PHP
// assertions are enabled or disable otherwise.
Runtime::auto();

默认情况下，框架不监听任何命名空间。要为您的应用程序添加命名空间，请使用Runtime::listen()方法。

use Serafim\Contracts\Runtime;

Runtime::listen('App\\Entity', 'App\\Http\\Controllers');

此外，您还可以指定缓存文件应存储的目录。

请注意，这些缓存文件由PHP包含，因此它们由opcache扩展缓存，不会降低性能。

use Serafim\Contracts\Runtime;

Runtime::cache(__DIR__ . '/storage');

用法

合同以嵌入属性中的引号字符串中的PHP代码形式编写。例如，#[Verify('$x < 100')]表示$x必须小于100。可以使用任何PHP表达式（匿名类除外），只要字符串被正确转义。

注解将合同绑定到代码元素：方法或类。库定义了三种主要注解类型，它们位于Serafim\Contracts\Attribute命名空间中

• #[Verify]用于方法先决条件；
• #[Ensure]用于方法后置条件；
• #[Invariant]用于类的不可变条件；

合同注解目前仅与类一起使用。

不变量

类可能具有关联的不可变条件。这些不可变条件不是在调用者和被调用者之间指定合同，而是描述了合格类型的有效对象的状态。对对象调用方法可能会使其发生变化；不可变条件保证在发生任何此类更改后，对象保持一致状态。

当然，内部操作允许临时破坏不可变条件以执行其工作，但它们同意最终将一切放回适当的位置。直观地说，对任何此类操作的任何操作都被认为是内部的，不需要遵守不可变条件。只有对其他变量的方法调用。

类中定义的任何不可变条件都可以访问其所有字段，包括任何受保护和私有的。

use Serafim\Contracts\Attribute\Invariant;

#[Invariant('$this->balance >= 0')]
class Account
{
    private int $balance = 0;
    
    public function deposit(int $amount): void
    {
        $this->balance += $amount + 1;
    }
}

在确定这种不可变条件时，账户余额将始终大于或等于零。

$account = new Account();

$account->deposit(42);      // OK
$account->deposit(-666);    // Serafim\Contracts\Exception\InvariantException: $this->balance >= 0

方法合同

方法可以附加先决条件和后置条件。共同，它们指定了调用者和被调用者之间的合同：如果方法进入时满足先决条件，则调用者可以假设在退出时满足后置条件。先决条件是被调用者对调用者的要求，而调用者期望在调用后保持后置条件。

以下是一个平方根函数的规范示例，该规范指出，对于给定的任何非负双精度浮点数x，sqrt将返回一个非负结果。

use Serafim\Contracts\Attribute\Verify;
use Serafim\Contracts\Attribute\Ensure;

class Math
{
    #[Verify('x >= 0')]
    #[Ensure('$result >= 0')]
    public static function sqrt(float $x): float 
    {
        // ...code
    }
}

如该示例所示，先决条件可以访问参数值；实际上，先决条件和后置条件是在它们绑定的方法上下文中评估的。更准确地说，每个注解的行为就像是一个方法，具有与合格方法相同的参数和作用域。在作用域方面，前面的代码等同于以下代码

use Serafim\Contracts\Attribute\Verify;
use Serafim\Contracts\Attribute\Ensure;

class Math
{
    public static function sqrt(float $x): float 
    {
        if ($x < 0) {
            throw new \Serafim\Contracts\Exception\PreconditionException('$x >= 0');
        }
        
        // ...code
        
        if ($result < 0) {
            throw new \Serafim\Contracts\Exception\PostconditionException('$result >= 0');
        }
        
        return $result;
    }
}

此外，后置条件可能包含一些扩展

• 正如我们所见，它们可能通过使用$result关键字来引用返回值。
• 在后置条件中，$old是一个关键字，包含对象变更前的状态。

在运行时，当启用契约时，前置条件和后置条件分别转换为对方法入口和退出的检查。失败会导致抛出PreconditionException或PostconditionException异常，具体取决于来源：未满足前置条件意味着方法被错误地调用，而未满足后置条件则指向方法实现本身的错误。

关键字

特性

• 类契约
  • 抽象方法
  • 继承（从父类、特性和接口导入）
• 特性契约
  • 抽象方法
• 接口契约