EiffelStudio如何生成启用contract校验的finalized可执行文件

可以实现保留所有前置条件、后置条件、类不变量同时生成Finalized优化级别的可执行文件，相比frozen with contracts模式性能提升明显，适配计算密集型应用的测试需求，操作方法如下：

• 如果你使用EiffelStudio图形界面：
  打开项目配置的「Compile」标签，找到「Assertions」设置分组，先取消勾选默认开启的「Strip assertions in finalized mode」选项，再依次勾选你需要保留的断言类型：Preconditions（前置条件）、Postconditions（后置条件）、Class invariants（类不变量）、Check instructions（check语句），最后选择Finalized模式编译即可。
• 如果你使用命令行ec工具编译：
  直接传入参数执行编译即可：ec -finalize -assertions all，该命令会开启Finalized模式的全量编译优化，同时保留所有类型的契约断言，性能远高于frozen with contracts模式。
• 额外性能优化技巧：
  如果仅需要对部分核心模块做契约校验，可以给不需要校验的类添加note assertion: "none"标注，编译时会自动跳过这些类的契约生成，进一步提升运行速度。也可以自定义需要保留的契约类型，比如命令行参数改为ec -finalize -assertions pre,post,invariant即可仅保留前置、后置、类不变量，去掉不需要的check语句校验，降低性能损耗。

内容的提问来源于stack exchange，提问作者Ilgiz Mustafin