当前位置：文江博客话题详情

在调用例程之后和之前在哪里评估不变量？

发布于 2024-11-15 08:34:02 字数 70 浏览 3 评论 0原文

在契约设计中，类不变量必须在两种情况下满足：创建对象之后和调用例程之后。是否有任何示例或条件，我也必须在调用例程之前进行评估？

原文

分享到QQ

分享到微博

如果你对这篇内容有疑问，欢迎到本站社区发帖提问参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。

发布评论

需要登录才能够评论，你可以免费注册一个本站的账号。

梦开始←不甜 2024-11-22 08:34:02

在功能调用之前可能会违反类不变量。情况可能有所不同，我只介绍最明显的情况：

混叠。一个对象引用类不变量中涉及的某个其他对象，并且该其他对象被第三方修改：

class SWITCH -- 为简洁起见，省略了创建过程。
特征
    toggle1、toggle2：TOGGLE——互斥的切换。
    ...
不变的
    切换1.is_on = 不是切换2.is_on
结尾

现在以下代码违反了类 SWITCH 的不变量：

switch.toggle1.turn_on -- 使 `switch.toggle1.is_on = True`
switch.toggle2.turn_on -- 使 `switch.toggle2.is_on = True`
switch.operate -- 在此调用之前违反了类不变式

外部状态。对象与类不变量中引用的外部数据耦合，并且可能会意外更改：

类 TABLE_CELL 功能
    项目：数据
        做
            结果 := 缓存 -- 尝试使用缓存值。
            如果没有附加结果则
                    -- 从数据库加载数据（慢）。
                结果 := 数据库.load_item (...)
                缓存 := 结果
            结尾
        结尾
功能 {NONE} -- 存储
    缓存：可分离的数据
不变的
    一致性缓存：--缓存包含最新值。
        附加缓存作为值所暗示的
        值〜database.load_item（...）
结尾

现在，如果在应用程序外部修改数据库，缓存可能会变得不一致，并在以下功能调用之前触发类不变性违规：

data := table_cell.item -- 在此调用之前违反了类不变量。

打回来。一个对象可以以无效状态传递给另一个对象：

类 HANDLER 功能
    流程（s：结构）
        做
            ... -- 一些将 `is_valid` 设置为 False 的代码。
            s.iterate_over_elements（当前）
        结尾
    流程元素（e：元素）
        做
            ...
        结尾
    is_valid: 布尔值
        做
            ...
        结尾
不变的
    有效
结尾

对 HADNLER 的回调（由 STRUCTURE 类的功能 iterate_over_elements 执行）会导致不变违规，因为 handler代码> 状态不佳：

handler.process_element (...) -- 在调用之前违反了类不变式。

人们可以说所有情况都是由于软件错误和缺陷造成的，但这正是类不变量捕获包括这些情况在内的情况的目的当违规时发生在功能调用之前。

The class invariant can be violated before a feature call. The conditions may be different, I'm presenting only the most obvious ones:

Aliasing. An object references some other object that is involved in a class invariant and that other object is modified by a third party:

class SWITCH -- Creation procedure is ommitted for brevity.
feature
    toggle1, toggle2: TOGGLE -- Mutually exclusive toggles.
    ...
invariant
    toggle1.is_on = not toggle2.is_on
end

Now the following code violates the invariant of class SWITCH:

switch.toggle1.turn_on -- Make `switch.toggle1.is_on = True`
switch.toggle2.turn_on -- Make `switch.toggle2.is_on = True`
switch.operate -- Class invariant is violated before this call

External state. An object is coupled with external data that is referenced in a class invariant and may change unexpectedly:

class TABLE_CELL feature
    item: DATA
        do
            Result := cache -- Attempt to use cached value.
            if not attached Result then
                    -- Load data from the database (slow).
                Result := database.load_item (...)
                cache := Result
            end
        end
feature {NONE} -- Storage
    cache: detachable DATA
invariant
    consistent_cache: -- Cache contains up-to-date value.
        attached cache as value implies
        value ~ database.load_item (...)
end

Now if the database is modified outside the application, the cache may become inconsistent and a class invariant violation is triggered before the following feature call:

data := table_cell.item -- Class invariant is violated before this call.

Callback. An object can be passed to the other one in an invalid state:

class HANDLER feature
    process (s: STRUCTURE)
        do
            ... -- Some code that sets `is_valid` to False.
            s.iterate_over_elements (Current)
        end
    process_element (e: ELEMENT)
        do
            ...
        end
    is_valid: BOOLEAN
        do
            ...
        end
invariant
    is_valid
end

A callback to HADNLER, performed by the feature iterate_over_elements of the class STRUCTURE, causes an invariant violation because handler is not in a good condition:

handler.process_element (...) -- Class invariant is violated before the call.

One can argue that all the cases are because of software bugs and flaws, but this is exactly the purpose of class invariants to catch those including the cases when the violation happens before feature calls.

回复收藏 0 原文

~没有更多了~