Links:
Atelier B (commercial) offers, within a coherent environment, numerous functionalities permitting the management of B projects in B language CafeOBJ a new generation algebraic specification and programming language CppSpec CppSpec is a behavior-driven development framework for C++. Using CppSpec, it is easy to write specifications for your code. Larch/C++ a notation for formally specifying the behavior and interfaces of C++ classes and functions Rapide designed to support component-based development of large, multi-language systems by utilizing architecture definitions as the development framework
