Depends on what aspect of object-oriented systems you want to specify. Can you be more precise? What exactly is it that you want to specify or verify and why is it that you want to combine semi-formal and formal methods?
Kim Mens, Thanks for the response. Usually the OO systems are specified using a set of models mostly by diagrams. I feel there is a need to specify the entire system more rigorously. There comes the need for formal methods. Many works I have come across using Z/Object Z with UML, Event B with UML etc. The objective of every such combination/integration is to increase the reliability of the software system.
I think that UML is a visual specification method but at the same time is not that strong to prove or disprove the system behaviors and its properties.
Event-B is a rigorous formal method for system specification. Rodin is an Eclipse-based IDE that provides tool support for Event-B. One Rodin plug-in is UML-B which, as its name suggests, combines UML and B. You may want to google Colin Snook (EECS/Univ Southampton), which is the main designer and maintainer of UML-B, I believe. He has also authored several papers on this approach.
I also recommend JML and Spec#. I think, the very good things about these languages are:
- The languages are Formal
- There are a wide range of tools available for verification , specification generation and other stuff related to the language
- Wide range of papers, specially for JML
- Active community for learning
- Also they are familiar to the developer. I think one reason that developers do not approach to formal methods is that mathematical rigorous ways are difficult to learn and developers are not comfortable with.
VDM++ can be used for the rigorous specification and verification of Object Oriented based development. VDM++ is an Object Oriented formal language. It is rigorous and ensures the correctness properties of the software. All types of properties can be specified by it.
It has a very efficient state of the art Eclipse based IDE tool named Overture. Overture is Open Source based on Eclipse and freely available for download.\