EiffelStudio 在启用合同的情况下完成

Question

如何生成启用合同检查的最终可执行文件？保持 check 语句完整是可能的，但是我们可以保持所有 pre/postconditions 和 class 不变量吗？

我需要这个来测试计算量大的应用程序，frozen with contracts 可执行文件在我的情况下有点太慢了。

Answer 1

IDE 显示了一个请求完成的对话框，询问是否应将断言保留在生成的可执行文件中。该对话框是可丢弃的。如果您 select 复选框“ 不再询问我 ”，将不会生成断言并且 IDE 将不再显示此对话框。您可以通过转到参数（例如，从主菜单：工具 | 参数）来重置此 selection，然后恢复Interface 下完成对话框的默认值 | 对话框.

在命令行中，编译器在 -finalize 之后接受一个选项 -keep。它告诉编译器在完成可执行文件时保留断言。

IDE 和编译器都选择应该从项目设置中生成断言的设置。您可以为每个组 (system/library/cluster) 和每个 class 单独指定它们。

编辑。这是一个包含 2 个文件的最小示例：

example.e:

class EXAMPLE create make feature
    make
        local
            n: INTEGER
        do
            if n = 0 then f
            elseif n = 1 then g
            end
        rescue
            n := n + 1
            print ({EXCEPTIONS}.tag_name)
            retry
        end
    f require pre: out = "x" do end
    g do ensure post: out = "x" end
end

example.ecf:

<?xml version="1.0" encoding="ISO-8859-1"?>
<system xmlns="http://www.eiffel.com/developers/xml/configuration-1-21-0" name="example">
    <target name="example">
        <root class="EXAMPLE" feature="make"/>
        <option>
            <assertions precondition="true" postcondition="true"/>
        </option>
        <setting name="console_application" value="true"/>
        <library name="base" location="$ISE_LIBRARY\library\base\base.ecf"/>
        <cluster name="test" location="."/>
    </target>
</system>

使用选项 -finalize -keep -config example.ecf -c_compile 编译生成打印 prepost.

的可执行文件

EiffelStudio 在启用合同的情况下完成

EiffelStudio finalize with contracts enabled

eiffel