米兰体育 Omnibus：一种干净的语言和支持工具，用于集成不同的基于断言的验证技术

引用

Wilson T、Maharaj S 和 Clark R (2005) Omnibus：一种干净的语言和支持工具，用于集成不同的基于断言的验证技术。见：Butler M、Jones C、Romanovsky A 和 Troubisyna E（编辑）容错系统严格工程研讨会论文集 (REFT 2005)。技术报告系列，CS-TR-915。容错系统严格工程研讨会 (REFT 2005)，纽卡斯尔，2005 年 7 月 19 日至 2005 年 7 月 19 日。泰恩河畔纽卡斯尔：泰恩河畔纽卡斯尔大学，第 43-52 页。 http://rodin.cs.ncl.ac.uk/REFT.htm

摘要
Omnibus 是一个用于开发可靠的面向对象软件的新系统。它包含一种干净的语言，表面上与 Java 类似，但删除了使验证特别复杂的方面。为运行时断言检查、扩展静态检查和完整形式验证提供集成支持。该语言由带有类型检查器、Java 代码生成器、HTML 文档生成器和一系列验证器的原型 IDE 支持。本文介绍了 Omnibus 的案例，概述了该语言和工具，并讨论了它与可靠系统开发的关系。