A micromodularity mechanism

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

A micromodularity mechanism

Full text

Pdf (251 KB)

Source

Foundations of Software Engineering archive
Proceedings of the 8th European software engineering conference held jointly with 9th ACM SIGSOFT international symposium on Foundations of software engineering table of contents

Vienna, Austria

Session: Specification table of contents

Pages: 62 - 73

Year of Publication: 2001

ISBN:1-58113-390-1

Also published in ...

Authors

Daniel Jackson	Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts,
Ilya Shlyakhter	Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts,
Manu Sridharan	Laboratory for Computer Science, Massachusetts Institute of Technology, Cambridge, Massachusetts,

Sponsors

SIGSOFT: ACM Special Interest Group on Software Engineering
CEPIS : Council of European Professional Informatics Societies
VIENUT : Vienna University of Technology

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 8, Downloads (12 Months): 29, Citation Count: 28

Additional Information:

abstract references cited by index terms 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/503209.503219 What is a DOI?

ABSTRACT

A simple mechanism for structuring specifications is described. By modelling structures as atoms, it remains entirely first-order and thus amenable to automatic analysis. And by interpreting fields of structures as relations, it allows the same relational operators used in the formula language to be used for dereferencing. An extension feature allows structures to be developed incrementally, but requires no textual inclusion nor any notion of subtyping. The paper demonstrates the flexibility of the mechanism by application in a variety of common idioms.

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	R. Duke, G. Rose and G. Smith. Object-Z:A Specification Language Advocated for the Description o Standards. SVRC Technical Report 94-45.The So tware Verification Research Centre, University of Queensland, Australia.
	2	John V.Guttag,James J.Horning,and Andres Modet. Report on the Larch Shared Language:Version 2.3. Technical Report 58,Compaq Systems Research Center, Palo Alto,CA,1990.
	3	Daniel Jackson, Automating first-order relational logic, Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications, p.130-139, November 06-10, 2000, San Diego, California, United States
	4	Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002 [doi>10.1145/505145.505149]
	5	Daniel Jackson , Ian Schechter , Hya Shlyahter, Alcoa: the alloy constraint analyzer, Proceedings of the 22nd international conference on Software engineering, p.730-733, June 04-11, 2000, Limerick, Ireland [doi>10.1145/337180.337616]
	6	Hossein Saiedian, An Invitation to Formal Methods, Computer, v.29 n.4, p.16-17, April 1996 [doi>10.1109/MC.1996.488298]
	7	Michael Jackson, Software requirements & specifications: a lexicon of practice, principles and prejudices, ACM Press/Addison-Wesley Publishing Co., New York, NY, 1995
	8	Cliff B. Jones, Systematic software development using VDM (2nd ed.), Prentice-Hall, Inc., Upper Saddle River, NJ, 1990
	9	K Jensen , N Wirth , A B Mickel , J F Miner, Pascal user manual and report; 3rd ed., Springer-Verlag New York, Inc., New York, NY, 1985
	10	K.Rustan M.Leino and Greg Nelson.Data abstraction and information hiding .Research Report 160,Compaq Systems Research Center,November 2000.
	11	Hector Levesque,Fiora Pirri,and Ray Reiter.Foundations or the Situation Calculus.Link~ping Electronic Articles in Computer and Information Science,ISSN 1401-9841,Vol. 3(1998),Nr.018.
	12	Robin Milner , Mads Tofte , Robert Harper, The definition of Standard ML, MIT Press, Cambridge, MA, 1990
	13	S.Owre,N.Shankar,J.M.Rushby,and D.W.J.Stringer- Calvert.PVS Language Reference.Computer Science Laboratory,SRI International,Menlo Park,CA,September 1999.
	14	J. M. Spivey, The Z notation: a reference manual, Prentice Hall International (UK) Ltd., Hertfordshire, UK, 1992
	15	Ian Toyn et al.Formal Specification -Z Notation -Syntax, Type and Semantics.Consensus Working Dra t 2.6 o the Z Standards Panel BSI Panel IST/5/-/19/2 (Z Notation). August 24,2000.
	16	Jim Woodcock , Jim Davies, Using Z: specification, refinement, and proof, Prentice-Hall, Inc., Upper Saddle River, NJ, 1996
	17	Jos Warmer , Anneke Kleppe, The object constraint language: precise modeling with UML, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1998
	18	Pamela Zave , Michael Jackson, Conjunction as composition, ACM Transactions on Software Engineering and Methodology (TOSEM), v.2 n.4, p.379-411, Oct. 1993 [doi>10.1145/158431.158438]

CITED BY 28

	Daniel Jackson, Alloy: a lightweight object modelling notation, ACM Transactions on Software Engineering and Methodology (TOSEM), v.11 n.2, p.256-290, April 2002
	Chandrasekhar Boyapati , Sarfraz Khurshid , Darko Marinov, Korat: automated testing based on Java predicates, ACM SIGSOFT Software Engineering Notes, v.27 n.4, July 2002
	Andreas Schaad , Jonathan Moffett, Separation, review and supervision controls in the context of a credit application process: a case study of organisational control principles, Proceedings of the 2004 ACM symposium on Applied computing, March 14-17, 2004, Nicosia, Cyprus
	Jonathan Edwards , Daniel Jackson , Emina Torlak, A type system for object models, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Greg Dennis , Robert Seater , Derek Rayside , Daniel Jackson, Automating commutativity analysis at the design level, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Sarfraz Khurshid , Darko Marinov , Daniel Jackson, An analyzable annotation language, ACM SIGPLAN Notices, v.37 n.11, November 2002
	Michael Huth, Mathematics for the exploration of requirements, ACM SIGCSE Bulletin, v.36 n.2, June 2004
	Jonathan Edwards , Daniel Jackson , Emina Torlak , Vincent Yeung, Faster constraint solving with subtypes, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Scaling Step-Wise Refinement, IEEE Transactions on Software Engineering, v.30 n.6, p.355-371, June 2004
	Brant Hashii, Lessons learned using alloy to formally specify MLS-PCA trusted security architecture, Proceedings of the 2004 ACM workshop on Formal methods in security engineering, October 29-29, 2004, Washington DC, USA
	Marcelo F. Frias , Juan P. Galeotti , Carlos G. López Pombo , Nazareno M. Aguirre, DynAlloy: upgrading alloy with actions, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
	Pamela Zave, Address translation in telecommunication features, ACM Transactions on Software Engineering and Methodology (TOSEM), v.13 n.1, p.1-36, January 2004
	Viktor Kuncak , Daniel Jackson, Relational analysis of algebraic datatypes, ACM SIGSOFT Software Engineering Notes, v.30 n.5, September 2005
	Tiago Massoni , Rohit Gheyi , Paulo Borba, A model-driven approach to formal refactoring, Companion to the 20th annual ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, October 16-20, 2005, San Diego, CA, USA
	Rohit Gheyi , Tiago Massoni , Paulo Borba, A rigorous approach for proving model refactorings, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering, November 07-11, 2005, Long Beach, CA, USA
	Marcelo F. Frias , Carlos G. López Pombo , Gabriel A. Baum , Nazareno M. Aguirre , Thomas S. E. Maibaum, Reasoning about static and dynamic properties in alloy: A purely relational approach, ACM Transactions on Software Engineering and Methodology (TOSEM), v.14 n.4, p.478-526, October 2005
	Felix Sheng-Ho Chang , Daniel Jackson, Symbolic model checking of declarative relational models, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Shin Nakajima , Tetsuo Tamai, Formal specification and analysis of JAAS framework, Proceedings of the 2006 international workshop on Software engineering for secure systems, May 20-21, 2006, Shanghai, China
	Robert Seater , Daniel Jackson, Problem frame transformations: deriving specifications from requirements, Proceedings of the 2006 international workshop on Advances and applications of problem frames, May 23-23, 2006, Shanghai, China
	Greg Dennis , Felix Sheng-Ho Chang , Daniel Jackson, Modular verification of code with SAT, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	Mana Taghdiri , Robert Seater , Daniel Jackson, Lightweight extraction of syntactic specifications, Proceedings of the 14th ACM SIGSOFT international symposium on Foundations of software engineering, November 05-11, 2006, Portland, Oregon, USA
	Ilya Shlyakhter, Generating effective symmetry-breaking predicates for search problems, Discrete Applied Mathematics, v.155 n.12, p.1539-1548, June, 2007
	Marcelo F. Frias , Carlos G. Lopez Pombo , Juan P. Galeotti , Nazareno M. Aguirre, Efficient Analysis of DynAlloy Specifications, ACM Transactions on Software Engineering and Methodology (TOSEM), v.17 n.1, p.1-34, December 2007
	Mana Taghdiri , Daniel Jackson, Inferring specifications to detect errors in code, Automated Software Engineering, v.14 n.1, p.87-121, March 2007
	Evan Martin , Tao Xie, Automated Test Generation for Access Control Policies via Change-Impact Analysis, Proceedings of the Third International Workshop on Software Engineering for Secure Systems, p.5, May 20-26, 2007
	Michael R. A. Huth , Radha Jagadeesan , David A. Schmidt, A domain equation for refinement of partial systems, Mathematical Structures in Computer Science, v.14 n.4, p.469-505, August 2004
	Julian Dolby , Mandana Vaziri , Frank Tip, Finding bugs efficiently with a SAT solver, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
	Claudia Pons , Diego Garcia, A Lightweight Approach for the Semantic Validation of Model Refinements, Electronic Notes in Theoretical Computer Science (ENTCS), v.220 n.1, p.43-61, December, 2008