rCOS

rCOS的全名是 “A Refinement Calculus for Object Systems”（對象精化演算系統），它是一種基於RUP（Rational United Process）過程的開發面向對象軟體的形式化方法。rCOS定義了一種用於描述面向對象程式設計結構的形式規範，稱為OOL規範語言，用它可以很好的定義面向對象的概念，如類，對象，繼承，引用等，並在此定義的基礎上利用求精規則從需求到分析到設計再到實現整個過程的求精化簡。

其特徵豐富，包括子類，引用類型，可見性，繼承，動態綁定，多態和局部變數嵌套聲明。用於推理驗證不同抽象層次上的面向對象軟體，包括規格說明，設計和程式。rCOS的語法包括面向對象系統，類聲明，命令和表達式，其主要語法同java類似。