Approximating unity

  • Jürgen Dingel
Regular Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1282)


A framework for the stepwise refinement of UNITY programs with local variables is proposed. It is centered around two preorders. The first one compares program components with respect to a given context. Aside from being context-sensitive, this order also allows the introduction of local variables. The second preorder compares program contexts with respect to their discriminating power. Using these two relations, program refinement arises as a form of assumption/commitment reasoning. An example illustrates the use of the framework and presents some proof rules.

The simple syntactic and semantic structure of UNITY allows for a natural game-theoretic characterization of the preorders used in the framework.


Concurrent Program Denotational Semantic Proof Rule Unity Program Silent Transition 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AJM94]
    S. Abramsky, R. Jaghadeesan, and P. Malacaria. Full abstraction for PCF (extended abstract). In TACS '94, volume LNCS 789, pages 1–15. Springer Verlag, 1994.Google Scholar
  2. [AS82]
    G. R. Andrews and F.B. Schneider. Concepts and notations for concurrent programming. Technical Report 82-520, Cornell University, Department of Computer Science, 1982.Google Scholar
  3. [Bro93]
    S.D. Brookes. Full abstraction for a shared-variable parallel language. In Proceedings 8th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1993.Google Scholar
  4. [CK95]
    P. Collette and E. Knapp. Logical foundations for compositional verification and development of concurrent programs in UNITY. In AMAST '95, LNCS 936, pages 353–367. Springer Verlag, 1995.Google Scholar
  5. [CM88]
    K.M. Chandy and J. Misra. Parallel program design: a foundation. Addison Wesley, 1988.Google Scholar
  6. [dBKPR91]
    F.S. de Boer, J.N. Kok, C. Palamidessi, and J.J.M.M. Rutten. The failure of failures in a paradigm of asynchronous communication. In CONCUR '91, pages 111–126. Springer Verlag, 1991.Google Scholar
  7. [Din96]
    J. Dingel. Modular verification of shared-variable concurrent programs. In CONCUR '96, pages 703–718. Springer Verlag, 1996.Google Scholar
  8. [Lar87]
    K. G. Larsen. A context dependent equivalence between processes. Theoretical Computer Science, 49(2):185–216, 1987.CrossRefMathSciNetGoogle Scholar
  9. [Liu89]
    Z. Liu. A semantic model for UNITY. Technical report, Computer Science Department, University of Warwick, 1989.Google Scholar
  10. [McC96]
    G. McCusker. Games and full abstraction for FPC. In Proceedings 11th Annual IEEE Symposium on Logic in Computer Science. IEEE Computer Society Press, June 1996.Google Scholar
  11. [Mor89]
    C. Morgan. The specification statement. ACM Transactions on Programming Languages and Systems, 10(3), January 1989.Google Scholar
  12. [QJ91]
    X. Qiwen and H. Jifeng. A theory of state-based parallel programming: Part I. In J. Morris, editor, 4th BCS-FAGS Refinement Workshop, 1991.Google Scholar
  13. [San90]
    B.A. Sanders. Stepwise refinement of mixed specifications of concurrent programs. In M. Broy and C.B. Jones, editors, Proceedings of IFIP Working Conference on Programming and Methods, pages 1–25. Elsevier Science Publishers (North Holland), May 1990.Google Scholar
  14. [San91]
    B.A. Sanders. Eliminating the substitution axiom from UNITY logic. Formal Aspects of Computing, 3(2), 1991.Google Scholar
  15. [Sin91]
    A.K. Singh. Parallel programming: Achieving portability through abstraction. In 11th International Conference on Distributed Computing Systems, May 1991.Google Scholar
  16. [Ste96]
    P. Stevens, December 1996. Private communication.Google Scholar
  17. [Sti96]
    C. Stirling. Games and modal mu-calculus. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Verlag, 1996. LNCS 1055.Google Scholar
  18. [UK93a]
    R.T. Udink and J.N. Kok. On the relation between UNITY properties and sequences of states. In Semantics: Foundations and Applications, pages 594–608. Springer Verlag, 1993.Google Scholar
  19. [UK93b]
    R.T. Udink and J.N. Kok. Two fully abstract models for UNITY. In CONCUR '93, pages 339–352. Springer Verlag, 1993.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1997

Authors and Affiliations

  • Jürgen Dingel
    • 1
  1. 1.School of Computer ScienceCarnegie Mellon UniversityPittsburghUSA

Personalised recommendations