UNITY has quite a number of variants, e.g. Sanders', Collete and Knapp's, Udink's, Prasetya's, and Misra's new UNITY --each extends or changes the classical UNITY with something useful.
Despite the differences, the main structure of the standard UNITY laws are typically preserved. !UNITY is a HOL library providing a general theory for UNITY. By instantiating it, a user can spawn his own concrete UNITY variant. Standard UNITY laws will be inherited for free, so people don't have to keep re-proving them each time a new variant is introduced.
Since !UNITY is HOL library, all laws it provides are mechanically verified!!
Code Download:
!UNITY version 2002. Require Taupo 6. It includes:
Documentation/papers:
I.S.W.B. Prasetya, T.E.J. Vos, S.D. Swierstra, A. Azurat. !UNITY: a Theory of General UNITY. Draft, 2002.
Notes:
The notation is plain ASCII. There is also very little syntax sugaring in !UNITY (most operators are in the prefix notation). I deliberately avoid sugaring for maintenance reason. The current HOL itself allows quite fancy syntax sugaring. If the user desires, sugaring can be always be defined on top of any sugar-free library.
The library won't include compositional reasoning for the UNION (parallel composition) operator, since the strength of such a reasoning may be tightly connected to the specific kind of UNITY you use.
However, as an application, we are currently using the !UNITY to create a UNITY variant with enhanced power to do compositional reasoning [in progress]. See also here.
The library does include some laws on 'conservative' compositions. A property is conservative with respect to a given composition operation if the property is preserved by the operation. This is of course a very strict kind of composition, but we have in the past cases where they are quite useful.