Abstract
The solution proposed by Sanders in [14] consists of eliminating the need of the substitution axiom from Unity in order to eliminate the unsoundness problem caused by this axiom in Unity without loss of completeness. Sander's solution is based on the strongest invariant concept and provides theoretical advantages by formally capturing the effects of the initial conditions on the properties of a program. This solution is less convincing from a practical point of view because it assumes proofs of strongest invariant in the meta-level. In this paper we reconsider this solution showing that the general concept of invariant is sufficient to eliminate the substitution axiom and to provide a sound and relatively complete proof system for Unity logic. The advantage of the new solution is that proofs of invariants are mechanized inside the Unity logic itself.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
K. R. Apt and E. R. Olderog. Verification of sequential and concurrent programs. Texts and Monographs in Computer Science. Springer-Verlag, 1991.
N. Brown and D. Mery. A Proof Environment for Concurrent Programs. In J. C. P Woodcock and P. G. Larsen, editors, FME'93: Industrial-Strength Formal Methods. Springer Verlag, 1993. Lecture Notes in Computer Science 670.
N. Brown. A Sound Mapping from Abstract Algorithms to Occam Programs. In Transputer Research And Applications Conference. 23–25 Octobre 1994 (University of Georgia, USA), IOS Press, pages 218–231.
N. Brown. Verification and Mapping of Unity programs into distributed architectures. Phd. thesis, Université de de Nancy I, France, October 1994.
K.M. Chandy and J. Misra. Parallel Program Design A Foundation. Addison-Wesley Publishing Company, 1988. ISBN 0-201-05866-9.
S.A. Cook. Soundness and completeness for an axiomatic system, for program verification. SIAM J. Comput., 7:70–90, 1978.
E. W. Dijkstra and C. S. Scholten. Predicate Calculus and Program Semantics. Texts and Monographs in Computer Science. Springer Verlag, 1990.
R. Gerth and A. Pnueli. Rooting UNITY. In acm, editor, Int. Workshop on Software Specification and Design, pages 11–19, 1989.
E. Knapp. An exercise in the formal derivation of parallel programs: Maximum flows in graphs. Transactions On Programming Languages and Systems, 12(2):203–223, 1990.
Z. Manna and A. Pnueli. The Temporal Logic of Reactive and Concurrent Systems. Springer-Verlag, 1991. ISBN 0-387-97664-7.
D. Mery. The ⊓ system as a development system for concurrent programs: ⊓. Theoretical Computer Science, 94(2):311–334, march 1992.
S. Owicki and L. Lamport. Proving liveness properties of concurrent programs. ACM TOPLAS, 4(3):455–495, july 1982.
S. Ramesh. On the completeness of modular proof systems. Information Processing Letters, 36:195–201, 1990.
B. A. Sanders. Eliminating the substitution axiom from unity logic. Formal Aspects of Computing, 3:189–205, 1991.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1995 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brown, N., Mokkedem, A. (1995). On mechanizing proofs within a complete proof system for Unity. In: Alagar, V.S., Nivat, M. (eds) Algebraic Methodology and Software Technology. AMAST 1995. Lecture Notes in Computer Science, vol 936. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60043-4_67
Download citation
DOI: https://doi.org/10.1007/3-540-60043-4_67
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-60043-5
Online ISBN: 978-3-540-49410-2
eBook Packages: Springer Book Archive