Applying 'design by contract'

1992/10/01 by Bertrand Meyer, B. Meyer · 2,127 citations
Computer Science · #Advanced Software Engineering Methodologies #Artificial intelligence #Computer science #Design by contract #Eiffel #Logic, programming, and type systems #Object (grammar) #Object-oriented design #Object-oriented programming #Programming language #Software #Software Engineering Research #Software construction #Software design #Software development #Software engineering

paper · doi:10.1109/2.161279

published in Computer 25(10), 40-51 (IEEE Computer Society)

openalex publication_date 1992/10/01 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

Methodological guidelines for object-oriented software construction that improve the reliability of the resulting software systems are presented. It is shown that the object-oriented techniques rely on the theory of design by contract, which underlies the design of the Eiffel analysis, design, and programming language and of the supporting libraries, from which a number of examples are drawn. The theory of contract design and the role of assertions in that theory are discussed.>

Cited by

• A manifesto for applicable formal methods
• Experience Report on Formally Verifying Parts of OpenJDK's API with KeY
• A compositional approach to verifying modular robotic systems
• Automating structural reliability analysis with a multi-agent large language model framework
• Specification-Driven Development as the Foundation of AI-Native Enterprise Software Engineering
• Faithful Autoformalization of Natural Language Assertions
• Semantic Properties for Lightweight Specification in Knowledgeable Development Environments
• Specification-Driven DevOps for Multi-Service Environments
• Safe Integration of Annotated Components in Open Source Projects
• Checking the HAL Interface Specification Continuously, Right from the Start
• Weakest Preconditions and Cumulative Subgoal Fulfillment: A Comparison
• Verifying Contracts for Perturbed Control Systems using Linear Programming
• Automated Debugging In Java Using OCL And JDI
• SurvBench: A Standardised Preprocessing Pipeline for Multi-Modal Electronic Health Record Survival Analysis
• Refinement Calculus of Reactive Systems
• State Field Coverage: A Metric for Oracle Quality
• FLAMES: Fine-tuning LLMs to Synthesize Invariants for Smart Contract Security
• Weakening Goals in Logical Specifications
• When Abstraction Breaks Physics: Rethinking Modular Design in Quantum Software
• Beyond Postconditions: Can Large Language Models infer Formal Contracts for Automatic Software Verification?
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation
• OCL contracts for the verification of model transformations
• Moldable Exceptions
• A refinement-based approach to safe smart contract deployment and evolution
• Formalizing smart contract design patterns with DCR graphs
• Extending Design by Contract for Aspect-Oriented Programming
• A Generic Model of Contracts for Embedded Systems
• Jartege: a Tool for Random Generation of Unit Tests for Java Classes
• Uncovering Systematic Failures of LLMs in Verifying Code Against Natural Language Specifications
• Solving Financial Regulatory Compliance Using Software Contracts
• A DbC Inspired Neurosymbolic Layer for Trustworthy Agent Design
• A Design Recipe and Recipe-Based Errors for Regular Expressions
• HyDRA: A Hybrid-Driven Reasoning Architecture for Verifiable Knowledge Graphs
• Impact of Code Context and Prompting Strategies on Automated Unit Test Generation with Modern General-Purpose Large Language Models
• Symbolic construction of GR(1) contracts for synchronous systems with full information
• A Compositional Approach to Diagnosing Faults in Cyber-Physical Systems
• LLMs and Fuzzing in Tandem: A New Approach to Automatically Generating Weakest Preconditions
• Automatic Generation of Precise and Useful Commutativity Conditions (Extended Version)
• Reasoning about External Calls
• Preventing Atomicity Violations with Contracts
• Why Nominal-Typing Matters in OOP
• Verifying Compositional Refinement of Assume/Guarantee Contracts using Linear Programming
• Formal Language Constraints for Markov Decision Processes
• Engaging Millennials into Learning Formal Methods
• OTS/CafeOBJ2JML: An attempt to combine Design By Contract with Behavioral Specifications
• Reasoning and Improving on Software Resilience against Unanticipated Exceptions
• Vérification d'assemblages de composants logiciels : Application aux modèles de composants UML2.0 et Ugatze
• Safely creating correct subclasses without seeing superclass code
• Modelling System of Systems Interface Contract Behaviour
• Behavioral subtyping through typed assertions
• Modular and verified automatic program repair
• Object-oriented Programming Laws for Annotated Java Programs
• Proving Non-Deterministic Computations in Agda
• AgentModernize: Preserving Business Logic in Legacy Modernization with Multi-Agent LLMs and Behavioral Specification Graphs
• Harness as an Asset: Enforcing Determinism via the Convergent AI Agent Framework (CAAF)
• Resume Means Resume: A Machine-Checked Conformance Contract for Checkpoint, Interrupt, and Resume Semantics in Workflow Persistence Layers
• Multiset of Agents in a Network for Simulation of Complex Systems
• The Challenges of the Digital Transformation in Education
• Methods for enhancing the reproducibility of biomedical research findings using electronic health records. [europepmc]
• Information-flow interfaces. [europepmc]
• A Scalable Approach to IoT Interoperability: The Share Pattern. [europepmc]
• ChemTorch: A Deep Learning Framework for Benchmarking and Developing Chemical Reaction Property Prediction Models. [europepmc]
• An Abstract Contract Theory for Programs with Procedures [europepmc]

Related

• A Systematic Mapping Study on Contract-based Software Design for Dependable Systems
• Seamless Object-Oriented Requirements
• Complete contracts through specification drivers
• A framework for the semantics of behavioral contracts
• Semantic Component Composition