article

Free access

Automating first-order relational logic

Author:

Daniel JacksonAuthors Info & Claims

ACM SIGSOFT Software Engineering Notes, Volume 25, Issue 6

Pages 130 - 139

https://doi.org/10.1145/357474.355063

Published: 01 November 2000 Publication History

Abstract

An automatic analysis method for first-order logic with sets and relations is described. A first-order formula is translated to a quantifier-free boolean formula, which has a model when the original formula has a model within a given scope (that is, involving no more than some finite number of atoms). Because the satisfiable formulas that occur in practice tend to have small models, a small scope usually suffices and the analysis is efficient.

The paper presents a simple logic and gives a compositional translation scheme. It also reports briefly on experience using the Alloy Analyzer, a tool that implements the scheme.

References

[1]

William Adjie-Winoto, Elliot Schwartz, Had Balakrishnan and Jeremy Lille),. The design and implementation of an intentional naming system. Proceedings of the 17th A CM Symposium on Operating Systems Principles (SOSP '99), Kiawah Island, South Carolina, December 1999.]]

Digital Library

[2]

Sten Agerhold and Peter Gorm Larsen. The IFAD VDM Tools: Lightweight Formal Methods. FM-Trends 1998: 326- 329.]]

Digital Library

[3]

The B-Tool- B-Core(UK) Ltd, Harwell, Oxfordshire, England. http://www.b-core.com/htool.html.]]

[4]

R.J. Bayardo Jr. and R. C. Schrag. Using CSP look-back techniques to solve real world SAT instances. Proc. of the 14th National Conf. on Artificial Intelligence, 203-208, 1997.]]

Digital Library

[5]

A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolic Model Checking without BDDs. Too/s and Algorithms for the Analysis and Construction of Systems (TACAS'99), LNCS 1579, Springer-Verlag, 1999.]]

Digital Library

[6]

J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill and L.J. Hwang, Symbolic model checking: 10 ~~ states and beyond. Information and Computation, Vol. 98, No. 2, pp. 142-170, June 1992.]]

Digital Library

[7]

Dan Craigen, Irwin Meisds and Mark Saaltink. Analysing Z Specifications with Z/EVES. Industrial-Strength Formal Methods in Practice, eds. J.p. Bowen and M.G. Hinchey, September 1999.]]

[8]

Craig A. Damon( Selective Enumeration- Phi) Thesis, School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, August 2000.]]

Digital Library

[9]

Martin Davis and Hilary Putnam. A computing procedure for quantification theory. Journal of the ACM, Vol. 7, pp. 202-215, 1960.]]

Digital Library

[10]

Michael D. Ernst, Todd D. Millstein and Daniel S. Weld. Automatic SAT-Compilation of Planning Problems. Proc. 15th International Joint Conference on Artificial Intelligence (IJCAI-97), Nagoya, Aichi, Japan, August 1997, pp. 1169- 1176.]]

[11]

Daniel Hazel, Paul Strooper and Owen Traynor. Possum: An Animator for the SUM Specification Language. Proceedings Asia-Pacific Software Engineering Conference and International Computer Science Conference, pages 42-51, IEEE Computer Society, December 1997.]]

Digital Library

[12]

M.A. Hewitt, C.M. O'Halloran and C.T. Sennett. Experiences with PiZA, an animator for Z. lOth International Conference of Z Users (ZUM'97), Reading, England, April 1997.]]

Digital Library

[13]

Gerard J. Holzmann. The Modal Checker Spin. IEEE Transactions on Software Engineering, Special issue on Formal Methods in Software Practice, Volume 23, Number 5, May 1997, 279-295.]]

Digital Library

[14]

Daniel Jackson. Nitpick: A Checkable Specification language. Proc. First ACM SIGSOFT Workshop on Formal Methods in Software Practice, San Diego, CA, January 1996, pp. 60-69.]]

[15]

Daniel Jackson. An Intermediate Design Language and its Analysis. Proc. ACM Conference on Foundations of Software Engineering, Florida, November 1998.]]

Digital Library

[16]

Daniel Jackson. Alloy: A Lightweight Object Modelling Notation. Technical Report 797, MIT Laboratory for Computer Science, Cambridge, MA, February 2000. Available at: http:llsdg.lcs.mit.edul~dnjlpublications.]]

[17]

Daniel Jackson and CraigA. Damon. NitpickReference Manual. CMU-CS-96-109. School of Computer Science, Carnegie Mellon University, Pittsburgh, PA, January 1996.]]

[18]

Daniel Jackson and Craig A. Damon. Elements of Style: Analyzing a Software Design Feature with a Counterexample Detector. IEEE Transactions on Software Engineering, Vol. 22, No. 7, July 1996, pp. 484-495.]]

Digital Library

[19]

Daniel Jackson, Somesh lha and CraigA. Damon. Isomorph-free Model Enumeration: A New Method for Checking Relational Specifications. A CM Transactions on Programming Languages and Systems, Vol. 20, No. 2, March 1998, pp. 302-343.]]

Digital Library

[20]

Daniel Jackson, Yuchung Ng and Jeannette Wing. A Nitpick Analysis of IPv6. To appear, FormalAspects of Computing.]]

[21]

Daniel Jackson, Ian Schechter and Ilya Shlyakhter. Alcoa: the Alloy Constraint Analyzer. Proc. International Conference on Software Engineering, Limerick, Ireland, June 2000.]]

Digital Library

[22]

Daniel Jackson and Kevin Sullivan. COM Revisited: Tool- Assisted Modelling and Analysis of Software Structures. Proc. Foundations of Software Engineering (FSE 2000), San Diego, CA, November 2000.]]

Digital Library

[23]

Daniel Jackson & Mandana Vaziri. Finding Bugs with a Constraint Solver. Proc. International Conference on Software Testing and Analysis (ISSTA 2000), Portland, OR, August 2000.]]

Digital Library

[24]

R.D. Knott and P. I. Krause. The Implementation of Z Specifications using Program Transformation Systems: The SuZan Project. The Unified Computation Laboratory, IMA Conference Series No 35 (Editors: C Rattray, R G Clark), Clarendon Press, Oxford, 1992, pgs 207-220.]]

Digital Library

[25]

Henry Kautz and Bart Sdman. Pushing the envelope: planning, propositional logic, and stochastic search. Proc. 5th National Conference on Artificial Intelligence, 1996, pp. 1194-1201.]]

[26]

Sarfraz Khurshid and Daniel Jackson. Exploring the Design of an Intentional Naming System with an Automatic Constraint Analyzer. Proc. Automated Software Engineering, Grenoble, France, September 2000.]]

Digital Library

[27]

J. Magee, N. Dulay, S. Eisenbach and J. Kramer. Specifying Distributed Software Architectures. Proceedings of Sth European Software Engineering Conference (ESEC 95), Sitges, Spain, September 1995]]

Digital Library

[28]

Sam Owre, John Rushby, Natarajan Shankar, and Friedrich yon Henke. Formal verification for fault-tolerant' architectures: Prolegomena to the design of PVS. IEEE Transactions on Software Engineering, 21 (2):107-125, February 1995.]]

Digital Library

[29]

D. Plaisted and S. Greenbaum. A structure-preserving clause form translation. Journal of Symbolic Computation, 2, 293- 304, 1986.]]

Digital Library

[30]

Rose Visual Modeling Tool. Rational Software Corporation, Cupertino, California. Inc.]]

[31]

Bart Selman, Henry Kautz and Brain Cohen. Noise strategies for improving local search. Proc. AAAI-94, pp. 337-343, 1994.]]

Digital Library

[32]

J.P.M. Silva and K.A. Sakallah. Grasp - A New Search Algorithm for Satisfiability. IEEE In ternational Conference on Computer Aided Design, San Jose, CA, November 1996, pp. 220-227.]]

Digital Library

[33]

John Slaney. Finder: Finite domai n enumerator, system description. Proc. 12th International Conference on Automated Deduction. Lecture Notes in Artifical Intelligence. Springer-Verlag, Berlin, 798-801.]]

Digital Library

[34]

I. Michael Spivey. TheZNotation:A Reference Manual. Second ed, Prentice Hall, 1992.]]

Digital Library

[35]

K.J. Sullivan, I. Socha and M. Marchukov. Using Formal Methods to Reason about Architecfural Standards. Proceedings of the International Conference on Software Engineering (ICSE97), Boston, Massachusetts, May 1997.]]

Digital Library

[36]

Alfred Tarski and Steven Givant. A Formalization of Set Theory Without Variables. American Mathematical Society, Colloquium Publications, Volume 41, 1987.]]

[37]

Axel van Lamsweerde, Robert Darimont and Emmanuel Letier. Managing Conflicts in Goal-Driven Requirements Engineering. IEEE Transactions on Software Engineering, Vol. 24, No. 1 I, November 1998.]]

Digital Library

[38]

Mandana Vaziri and Daniel Jackson. Some Shortcomings of OCL, the Object Constraint Language of UML. A response to Object Management Group RFI on UML. December 1999. Available at: http:llsdg.lcs.mit.edul~dnjlpublications.]]

[39]

los Warmer and Anneke Kleppe. The Object Constraint Language: Precise Modeling with UML. Addison-Wesley, 1999.]]

Digital Library

[40]

David S. Wile. AML: An Architecture Meta-Language. Automated Software Engineering, 14th IEEE International Conference, Cocoa Beach,Florida, USA, October 1999.]]

Digital Library

[41]

Hantao Zhang. SATO: An Efficient Propositional Prover. Proc. of International Conference on Automated Deduction (CADE-97).]]

Digital Library

[42]

Hantao Zhang and Mark E. Stickel. Implementing the Davis- Putnam Algorithm by Tries. Technical Report 94-12, Artificial Intelligence Center, SRI International, Menlo Park, CA. December 1994.]]

[43]

Jia Xiaoping. An Approach to Animating Z Specifications. Proceedings of the 19th Annual IEEE International Computer Software and Application Conference (COMPSAC'95). August 1995, Dallas, TX. pp. 108-113.]]

Digital Library

Cited By

Haas TMeyer RPonce de León H(2022)CAAT: consistency as a theoryProceedings of the ACM on Programming Languages10.1145/35632926:OOPSLA2(114-144)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563292
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582
Sylla AGuillouard KKlamm FOuzzif MMerle PRayana SStefani J(2019) Formal Verification of Orchestration Templates for Reliable Deployment with OpenStack Heat * 2019 15th International Conference on Network and Service Management (CNSM)10.23919/CNSM46954.2019.9012739(1-5)Online publication date: Oct-2019
https://doi.org/10.23919/CNSM46954.2019.9012739
Show More Cited By

Index Terms

Automating first-order relational logic
1. Software and its engineering
  1. Software creation and management
    1. Designing software
      1. Software implementation planning
        Software design techniques
    2. Software development process management
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Automating first-order relational logic
SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications

An automatic analysis method for first-order logic with sets and relations is described. A first-order formula is translated to a quantifier-free boolean formula, which has a model when the original formula has a model within a given scope (that is, ...
Formalization of the Resolution Calculus for First-Order Logic

I present a formalization in Isabelle/HOL of the resolution calculus for first-order logic with formal soundness and completeness proofs. To prove the calculus sound, I use the substitution lemma, and to prove it complete, I use Herbrand interpretations ...
First-Order Logic in the Medvedev Lattice

Kolmogorov introduced an informal calculus of problems in an attempt to provide a classical semantics for intuitionistic logic. This was later formalised by Medvedev and Muchnik as what has come to be called the Medvedev and Muchnik lattices. However, ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGSOFT Software Engineering Notes

ACM SIGSOFT Software Engineering Notes Volume 25, Issue 6

Nov. 2000

169 pages

ISSN:0163-5948

DOI:10.1145/357474

Editors:
Will Tracz
Lockheed Martin Federal systems, Owego, NY
,
David S. Rosenblum
Univ. of California, Irvine

Issue’s Table of Contents

SIGSOFT '00/FSE-8: Proceedings of the 8th ACM SIGSOFT international symposium on Foundations of software engineering: twenty-first century applications
November 2000
170 pages
ISBN:1581132050
DOI:10.1145/355045
Chairman:
John C. Knight
Univ of Virginia
,
Editor:
David S. Rosenblum
Univ of California, Irvine

Copyright © 2000 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 November 2000

Published in SIGSOFT Volume 25, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

158
Total Citations
View Citations
1,281
Total Downloads

Downloads (Last 12 months)107
Downloads (Last 6 weeks)21

Reflects downloads up to 07 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Haas TMeyer RPonce de León H(2022)CAAT: consistency as a theoryProceedings of the ACM on Programming Languages10.1145/35632926:OOPSLA2(114-144)Online publication date: 31-Oct-2022
https://dl.acm.org/doi/10.1145/3563292
Kulik TDongol BLarsen PMacedo HSchneider STran-Jørgensen PWoodcock J(2022)A Survey of Practical Formal Methods for SecurityFormal Aspects of Computing10.1145/352258234:1(1-39)Online publication date: 5-Jul-2022
https://dl.acm.org/doi/10.1145/3522582
Sylla AGuillouard KKlamm FOuzzif MMerle PRayana SStefani J(2019) Formal Verification of Orchestration Templates for Reliable Deployment with OpenStack Heat * 2019 15th International Conference on Network and Service Management (CNSM)10.23919/CNSM46954.2019.9012739(1-5)Online publication date: Oct-2019
https://doi.org/10.23919/CNSM46954.2019.9012739
Souaf SLoulergue F(2019)A First Step in the Translation of Alloy to CoqFormal Methods and Software Engineering10.1007/978-3-030-32409-4_28(455-469)Online publication date: 28-Oct-2019
https://doi.org/10.1007/978-3-030-32409-4_28
邹科(2017)Automated Verification of Equivalence of Two Group Definitions Based on AlloyAdvances in Applied Mathematics10.12677/AAM.2017.6912706:09(1050-1055)Online publication date: 2017
https://doi.org/10.12677/AAM.2017.69127
徐月(2017)Machine Verification of the Existence Theorem of Configuration 7₃ Based on AlloyAdvances in Applied Mathematics10.12677/AAM.2017.6812306:08(1027-1033)Online publication date: 2017
https://doi.org/10.12677/AAM.2017.68123
Shaikh RAdi KLogrippo L(2017)A Data Classification Method for Inconsistency and Incompleteness Detection in Access Control Policy SetsInternational Journal of Information Security10.1007/s10207-016-0317-116:1(91-113)Online publication date: 1-Feb-2017
https://dl.acm.org/doi/10.1007/s10207-016-0317-1
Tanhaei MHabibi JMirian-Hosseinabadi S(2016)Automating feature model refactoringInformation and Software Technology10.1016/j.infsof.2016.08.01180:C(138-157)Online publication date: 1-Dec-2016
https://dl.acm.org/doi/10.1016/j.infsof.2016.08.011
SHIMAKAWA MHAGIHARA SYONEZAKI N(2013)Complexity of Strong Satisfiability Problems for Reactive System SpecificationsIEICE Transactions on Information and Systems10.1587/transinf.E96.D.2187E96.D:10(2187-2193)Online publication date: 2013
https://doi.org/10.1587/transinf.E96.D.2187
Mu KJin ZLiu WZowghi DWei B(2013)Measuring the significance of inconsistency in the Viewpoints frameworkScience of Computer Programming10.1016/j.scico.2012.12.00678:9(1572-1599)Online publication date: Sep-2013
https://doi.org/10.1016/j.scico.2012.12.006
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Issue’s Table of Contents