Tentative steps toward a development method for interfering programs

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Tentative steps toward a development method for interfering programs

Full text

Pdf (1.33 MB)

Source

ACM Transactions on Programming Languages and Systems (TOPLAS) archive
Volume 5 , Issue 4 (October 1983) table of contents

Pages: 596 - 619

Year of Publication: 1983

ISSN:0164-0925

Author

C. B. Jones

Manchester University

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 18, Downloads (12 Months): 80, Citation Count: 36

Additional Information:

references cited by index terms review collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/69575.69577 What is a DOI?

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Jean-Raymond Abrial , Stephen A. Schuman, Non-Deterministic System Specification, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.34-50, July 02-04, 1979
	2	ACZEL, P. A note on program verification. Private communication, Jan. 1982.
	3	Krzysztof R. Apt , Nissim Francez , Willem P. de Roever, A Proof System for Communicating Sequential Processes, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.3, p.359-385, July 1980 [doi>10.1145/357103.357110]
	4	BURSTALL, R.M. Program proving as hand simulation with a little induction. In Proceedings, IFIP Congress 1974. ELsevier North-Holland, New York, 1974, pp. 308-312.
	5	Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
	6	Edsger W. Dijkstra , Leslie Lamport , A. J. Martin , C. S. Scholten , E. F. M. Steffens, On-the-fly garbage collection: an exercise in cooperation, Communications of the ACM, v.21 n.11, p.966-975, Nov. 1978 [doi>10.1145/359642.359655]
	7	FLOYD, R.W. Assigning meanings to programs. In Proceedings of 19th Symposium on Applied Mathematics. American Mathematical Society, Providence, R.I., 1967, pp. 19-31.
	8	FRANCEZ, N., ANn PNUELI, A. A proof method for cyclic programs. Acta Inf. 9, 2 (Apr. 1978), 133-157.
	9	R. T. Hailpern, Verifying Concurrent Processes Using Temporal Logic, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	10	C. A. R. Hoare, Communicating sequential processes, Communications of the ACM, v.21 n.8, p.666-677, Aug. 1978 [doi>10.1145/359576.359585]
	11	C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
	12	HOARE, C.A.R. Proof of correctness of data representations. Acta Inf. 1, 4 (Nov. 1972), 271-281.
	13	C. A. R. Hoare, Proof of a program: FIND, Communications of the ACM, v.14 n.1, p.39-45, Jan. 1971 [doi>10.1145/362452.362489]
	14	C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
	15	M. A Jackson, System development (Prentice-Hall International series in computer science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1983
	16	JONES, C.B. Development methods for computer programs including a notion of interference. Tech. Rep. PRG 25, Programming Research Group, Oxford Univ., Oxford, Eng., 1981.
	17	C. B. Jones, Towards More Formal Specifictations, Software Engineering - Entwurf und Spezifikation, Tagung II/1980 mit Workshop des German Chapter of the ACM, p.19-45, September 12-16, 1980
	18	Cliff B. Jones, Software Development: A Rigorous Approach, Prentice Hall PTR, Upper Saddle River, NJ, 1980
	19	JONES, C.B. Constructing a theory of a data structure as an aid to program development. Acta Inf. 11, 2 (Jan. 1979), 119-137.
	20	JONES, C.B. Formal development of programs. Tech. Rep. TR 12.117, IBM Hursley Laboratory, England, June 1973.
	21	C B Jones, Formal development of correct algorithms: An example based on earley's recogniser, Proceedings of ACM conference on Proving assertions about programs, p.150-169, January 06-07, 1972, Las Cruces, New Mexico, United States
	22	KAHN, G. A preliminary theory for parallel programs. Tech. Rep. 6, IRIA, Le Chesnay, France, 1973.
	23	LAMPORT, L. The "Hoare logic" of concurrent programs. Acta Inf. 14, 1 (June 1980), 21-37.
	24	LAUER, P.E. Consistent formal theories of the semantics of programming languages. Tech. Rep TR25.121, IBM Laboratory Vienna, Nov. 1971.
	25	LEVIN, G.M., AND GRIES, D. A proof technique for communicating sequential processes. Acta Inf. 15, 3 (June 1981), 281-302.
	26	Zohar Manna, Properties of Programs and the First-Order Predicate Calculus, Journal of the ACM (JACM), v.16 n.2, p.244-255, April 1969 [doi>10.1145/321510.321516]
	27	Zohar Manna , Amir Pnueli, The Modal Logic of Programs, Proceedings of the 6th Colloquium, on Automata, Languages and Programming, p.385-409, July 16-20, 1979
	28	R. Milner, A Calculus of Communicating Systems, Springer-Verlag New York, Inc., Secaucus, NJ, 1982
	29	Robin Milner, An algebraic definition of simulation between programs, Stanford University, Stanford, CA, 1971
	30	MORRIS, J.H., JR. A correctness proof using recursively defined functions. In Formal Semantics of Programming Languages, R. Rustin (Ed.). Prentice-Hall, Englewood Cliffs, N.J., 1972.
	31	NAUR, P. Proof of algorithms by general snapshots. BIT 6 (1966), 310-316.
	32	Susan S. Owicki, Axiomatic Proof Techniques for Parallel Programs, Cornell University, Ithaca, NY, 1975
	33	Susan Owicki , David Gries, Verifying properties of parallel programs: an axiomatic approach, Communications of the ACM, v.19 n.5, p.279-285, May 1976 [doi>10.1145/360051.360224]
	34	PLOTKIN, G.D. A power domain construction. SIAMJ. Comput. 5, 3 (Sept. 1976), 452-487.
	35	Amir Pnueli, The Temporal Semantics of Concurrent Programs, Proceedings of the International Sympoisum on Semantics of Concurrent Computation, p.1-20, July 02-04, 1979
	36	SMYTH, M.B. Power domains. J. Comput. Syst. Sci. 16 (1978), 23-36.
	37	U.S. DEPT. OF DEFENSE. Reference Manual for the Ada Programming Language (Proposed standard document). July 1980.
	38	VON LAMSWEERDE, A., AND SINTZOFF, M. Formal derivation of strongly correct parallel programs. Tech. Rep. R338, MBLE, Belgium, Oct. 1976.
	39	Niklaus Wirth, Program development by stepwise refinement, Communications of the ACM, v.14 n.4, p.221-227, April 1971 [doi>10.1145/362575.362577]
	40	ZHOU, C.C., AND HOARE, C.A.R. Partial correctness of Communicating sequential processes. In Proceedings, 2d International Conference on Distributed Computing Systems (Apr. 1981).
	41	ZHOU, C.C., A~D HOARE, C.A.R. Partial correctness of communicating processes and protocols. Tech. Rep. PRG-20, Programming Research Group, Oxford Univ., Oxford, Eng., 1981.

CITED BY 36

	Farokh Bastani , Wael Hilal , Ing-Ray Chen, Performance analysis of concurrent maintenance policies for servers in a distributed environment, Proceedings of 1986 ACM Fall joint computer conference, p.611-619, November 1986, Dallas, Texas, United States
	D. Garlan , S. Jha , D. Notkin , J. Dingel, Reasoning about implicit invocation, ACM SIGSOFT Software Engineering Notes, v.23 n.6, p.209-221, Nov. 1998
	Prakash Krishnamurthy , Paolo A. G. Sivilotti, The specification and testing of quantified progress properties in distributed systems, Proceedings of the 23rd International Conference on Software Engineering, p.201-210, May 12-19, 2001, Toronto, Ontario, Canada
	Peter T. Breuer , Carlos Kloos Delgado , Andrés López Marín , Natividad Martínez Madrid , Luis Sánchez Fernández, A refinement calculus for the synthesis of verified hardware descriptions in VHDL, ACM Transactions on Programming Languages and Systems (TOPLAS), v.19 n.4, p.586-616, July 1997
	Juergen Dingel, Computer-assisted assume/guarantee reasoning with VeriSoft, Proceedings of the 25th International Conference on Software Engineering, May 03-10, 2003, Portland, Oregon
	Paolo A. G. Sivilotti , Charles P. Giles, The specification of distributed objects: liveness and locality, Proceedings of the 1999 conference of the Centre for Advanced Studies on Collaborative research, p.11, November 08-11, 1999, Mississauga, Ontario, Canada
	Kenneth R. Wood, A pragmatic basis for the formal development of distributed systems, Proceedings of the 7th international workshop on Software specification and design, December 06-07, 1993, Redondo Beach, California
	A. Moitra , S. S. Iyengar , F. B. Bastani , I. L. Yen, Multilevel Data Structures: Models and Performance, IEEE Transactions on Software Engineering, v.14 n.6, p.858-867, June 1988
	Bruno Mermet , Dominique Méry, Service specifications: to B, or not to B, Proceedings of the second workshop on Formal methods in software practice, p.62-69, March 04-05, 1998, Clearwater Beach, Florida, United States
	Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Race checking by context inference, ACM SIGPLAN Notices, v.39 n.6, May 2004
	Andrew Kay , Joy N. Reed, A Rely and Guarantee Method for Timed CSP: A Specification and Design of a Telephone Exchange, IEEE Transactions on Software Engineering, v.19 n.6, p.625-639, June 1993
	Dachuan Yu , Zhong Shao, Verification of safety properties for concurrent assembly code, ACM SIGPLAN Notices, v.39 n.9, September 2004
	Sung Kim , Farokh B. Bastani , I-Ling Yen , Ing-Ray Chen, Systematic Reliability Analysis of a Class of Application-Specific Embedded Software Frameworks, IEEE Transactions on Software Engineering, v.30 n.4, p.218-230, April 2004
	Rimvydas Rukšenas, A rigorous environment for development of concurrent systems, Nordic Journal of Computing, v.11 n.2, p.165-193, Summer 2004
	Cormac Flanagan , Stephen N. Freund , Shaz Qadeer , Sanjit A. Seshia, Modular verification of multithreaded programs, Theoretical Computer Science, v.338 n.1-3, p.153-183, 10 June 2005
	Mohammad Zulkernine , Rudolph Seviora, Towards automatic monitoring of component-based software systems, Journal of Systems and Software, v.74 n.1, p.15-24, January 2005
	Xinyu Feng , Zhong Shao, Modular verification of concurrent assembly code with dynamic thread creation and termination, ACM SIGPLAN Notices, v.40 n.9, September 2005
	Xinyu Feng , Zhong Shao , Alexander Vaynberg , Sen Xiang , Zhaozhong Ni, Modular verification of assembly code with stack-based control abstractions, ACM SIGPLAN Notices, v.41 n.6, June 2006
	F. B. Bastani , V. Reddy , P. Srigiriraju , I.-L. Yen, Systematic validation of a relational control program for the bay area rapid transit system, High integrity software, Kluwer Academic Publishers, Norwell, MA, 2001
	I-Ling Yen , Farokh B. Bastani , David J. Taylor, Design of Multi-Invariant Data Structures for Robust Shared Accesses in Multiprocessor Systems, IEEE Transactions on Software Engineering, v.27 n.3, p.193-207, March 2001
	Jörg Kienzle , Shane Sendall, Addressing concurrency in object-oriented software development, Proceedings of the 2006 conference of the Center for Advanced Studies on Collaborative research, October 16-19, 2006, Toronto, Ontario, Canada
	Jozef Hooman , Jaco van de Pol, Semantic models of a timed distributed dataspace architecture, Theoretical Computer Science, v.331 n.2-3, p.291-323, 25 February 2005
	Claudio de la Riva , Javier Tuya, Automatic generation of assumptions for modular verification of software specifications, Journal of Systems and Software, v.79 n.9, p.1324-1340, September 2006
	Andrew McCreight , Zhong Shao , Chunxiao Lin , Long Li, A general framework for certifying garbage collectors and their mutators, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Shriram Krishnamurthi , Kathi Fisler, Foundations of incremental aspect model-checking, ACM Transactions on Software Engineering and Methodology (TOSEM), v.16 n.2, p.7-es, April 2007
	Xinyu Feng , Zhaozhong Ni , Zhong Shao , Yu Guo, An open framework for foundational proof-carrying code, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France
	Raffi Khatchadourian , Johan Dovland , Neelam Soundarajan, Enforcing behavioral constraints in evolving aspect-oriented programs, Proceedings of the 7th workshop on Foundations of aspect-oriented languages, p.19-28, April 01-01, 2008, Brussels, Belgium
	Ravi Chugh , Jan W. Voung , Ranjit Jhala , Sorin Lerner, Dataflow analysis for concurrent programs using datarace detection, ACM SIGPLAN Notices, v.43 n.6, June 2008
	C. B. Jones, Splitting atoms safely, Theoretical Computer Science, v.375 n.1-3, p.109-119, May, 2007
	R. Banach , M. Poppleton , C. Jeske , S. Stepney, Engineering and theoretical underpinnings of retrenchment, Science of Computer Programming, v.67 n.2-3, p.301-329, July, 2007
	Dimitra Giannakopoulou , Corina S. Păsăreanu , Howard Barringer, Component Verification with Automatically Generated Assumptions, Automated Software Engineering, v.12 n.3, p.297-320, July 2005
	Kohei Honda , Nobuko Yoshida, A uniform type structure for secure information flow, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.6, p.31-es, October 2007
	Sagar Chaki , Edmund Clarke , Natasha Sharygina , Nishant Sinha, Verification of evolving software via component substitutability analysis, Formal Methods in System Design, v.32 n.3, p.235-266, June 2008
	Ji Zhang , Heather J. Goldsby , Betty H.C. Cheng, Modular verification of dynamically adaptive systems, Proceedings of the 8th ACM international conference on Aspect-oriented software development, March 02-06, 2009, Charlottesville, Virginia, USA
	Xinyu Feng, Local rely-guarantee reasoning, Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 21-23, 2009, Savannah, GA, USA
	Xinyu Feng , Zhong Shao , Yu Guo , Yuan Dong, Certifying Low-Level Programs with Hardware Interrupts and Preemptive Threads, Journal of Automated Reasoning, v.42 n.2-4, p.301-347, April 2009

INDEX TERMS

Primary Classification:
D. Software
D.1 PROGRAMMING TECHNIQUES

Additional Classification:
D. Software
D.2 SOFTWARE ENGINEERING
D.2.1 Requirements/Specifications
Subjects: Methodologies (e.g., object-oriented, structured); Languages
D.3 PROGRAMMING LANGUAGES
D.3.2 Language Classifications

Nouns: Ada

F. Theory of Computation
F.3 LOGICS AND MEANINGS OF PROGRAMS

General Terms:
Design, Languages, Performance, Theory, Verification

REVIEW

"Randal P. Leavitt : Reviewer"

C. B. Jones has produced a very interesting report. It summarizes the work done during his two year stay at Oxford, and illustrates the extension of his rigorous software development method to include the programming of concurrent processes. The more...

Collaborative Colleagues:

C. B. Jones: colleagues

Adobe Acrobat

QuickTime

Windows Media Player

Real Player