[Wishnu Prasetya Home]

Its a HOL theory of that extends UNITY with compositional reasoning for mutual exclusion based distributed systems. Every UNITY properties (operators) now get two extra parameters, and they give you convenient laws to compose programs/properties. You get much more that the usual UNLESS and ENSURES compositionality laws.

Code Download:

1. Feb 2002 Build, for HOL Taupo 6.

2. June 1999 Build, for HOL98 Atabascha 2.

   There is also an example. Here is the result. And here is a paper discussing the example. The theory itself is described in the papers below.

Theorems Listing:

1. Listing of Theorems 1
2. Listing of Theorems 2

1. I.S.W.B. Prasetya, S.D. Swierstra, B. Widjaja. Component-wise Formal Approach to Design Distributed Systems (Original). 1999, Draft.

2. Here is our most recent paper. The presentation is much nicer, and it also discusses about things like generalization and verification. However, some notions are called differently here.

   I.S.W.B. Prasetya, T.E.J. Vos, S.D. Swierstra, B. Widjaja. A Theory for Composing Distributed Components Based on Mutual Exclusion. Draft, 2002. Submitted for publication.