Ceagle提供丰富的信息以展示完整的验证结果。在网页版和命令行版中这些信息的展示存在一些细节上的差别。
- 验证结论:Ceagle对给定属性进行验证的结果。验证结论可能的情况有TRUE、FALSE和UNKNOWN。属性成立的情形结论为TRUE。属性不成立的情形结论为FALSE。程序中存在不支持的特性,或者受限于程序的复杂性和验证引擎的计算能力而不能有效的判断属性成立与否的情形,Ceagle将给出UNKNOWN作为验证结论。
- 反例:验证结论为FALSE的情形,Ceagle会给出一条导致属性不成立的程序执行路径作为反例。在网页版中反例将直接展示在程序代码中,在命令行版中反例会以源代码中的行号展示。
- 运行信息:开发者可以选择查看Ceagle完成验证任务消耗的时间和资源以及验证过程的中间信息。
- 多属性验证:当验证任务包含多条属性时,Ceagle会针对每个属性给出结果信息,并以表格形式整理提供。