Design by contract

Question 1

JML – Java Modelling Language

Answer 1

• formal specification language for sequential Java by
  Gary Leavens et. al.
• – to specify behaviour of Java classes & interfaces
• – to record detailed design decisions
• by adding annotations to Java source code in Design-
  By-Contract style, using eg. pre/postconditions and
  invariants
• Design goal: meant to be usable by any Java
  programmer

Question 2

design by contract

Answer 2

Introduction & Origin:

Design by Contract is formally a “software correctness” testing methodology: a set of principles and methodologies based on defining a “contract” between classes and the way their methods are called. These “contracts” are then used to ensure software correctness by testing and asserting the validity of the protocols specified in the contract.

It was originally introduced by French academician Bertrand Meyer in 1986 in his programming language Eiffel, but has since been adopted into several other languages, and proves to be especially useful in game programming.
Contracts:

Imagine a business setting, where you have a client and a supplier. The client intends to obtain a certain product from the supplier in exchange for a pre-determined payment and the supplier must in turn develop the product according to the specifications of the client. This forms a contract: a sort of binding that defines the interactions of the supplier and the client.

This is precisely what DbC strives to do: to design a contract, or interaction protocol, between classes and methods. It achieves this by the use of three concepts:

Preconditions: Preconditions are the requirements that must be true when any function is called. These are conditions that the called function asserts must be true for it to operate correctly and the caller must ensure these. Examples include testing of input validity and certain class states.
Postconditions: Postconditions are the conditions that hold true once the called function is completed. These must hold true at the end of the function and are asserted by the called function and occasionally by the caller.
Invariants: Invariants are classes or properties that should not change as a result of the interaction between the contract participants. These differ from the conditions primarily in the form of scope, with invariants generally being class level in scope.

Contracts, in the context of DbC, find inspiration from a formal system called the Hoare Triple or Hoare Logic System. The Hoare Logic System states that we can quantify the “correctness” of a program by discussing how a computation changes the state of the system; represented in equation form it looks like this:

{P} C {Q}

where P represents a pre condition, C represents a computation, and Q represents a post condition.

So what should happen if someone does violate this contract? Well, in the business setting, they would probably sue each other.

However, DbC dictates that contract violation leads to undefined behavior or program termination. Basically, if the pre or post conditions are not met, or the invariants don’t hold true, then the program must stop execution and report this violation.

So what good do contracts really do tho? I feel that their most powerful benefit is a clear rationale for system design and development, as explained by the tutorial for DbC at Eiffel’s very own site:

What are contracts good for? Their first use is purely methodological. By applying a discipline of expressing, as precisely as possible, the logical assumptions behind software elements, you can write software whose reliability is built-in: software that is developed hand-in-hand with the rationale for its correctness.

This simple observation — usually not clear to people until they have practiced Design by Contract™ thoroughly on a large-scale project — brings as much change to software practices and quality as the rest of object technology.

As a design paradigm:

DbC is easily contrasted with an another design paradigm called “Defensive Programming”. In defensive programming, the called function must handle input incorrectness (amongst all other preconditions and post conditions) and provide appropriate behavior, even on violation of the contract. This often leads to a lot of unnecessary code in the form of tests for validity on both sides of the contract participants, and has a higher development cost. It is also associated with a potential veiling of programming errors. However, it is useful for fault tolerant systems, or unreliable client-server setups that can have requests that fail, but must not have the program stop its execution.

In DbC, by clearly defining the parameters of the interaction, we avoid all the code involved in tests and reduce the development time. With clear reporting of errors, we are also able to go back and correct the programming errors. It also promotes code readability by virtue of clearly stating contract expectations.
Designing a class Dictionary in Eiffel

The above is a code snippet from the DbC Eiffel Tutorial page showcasing the definition of a class Dictionary in Eiffel, with a feature (a method) called put with two parameters, an ELEMENT x, and a STRING key.

In Eiffel, the require keyword specifies preconditions, ensure specifies post conditions, and the keyword invariant specifies invariants, conditions that hold true for a class throughout computations. For the put method, the method requires the the preconditions that the count be less than or equal to capacity and the key parameter not be empty. After execution, the method ensures that the class has an item x, and that fetching the item associated with the key retrieves x, as well as that the count is incremented by 1. Throughout the execution, the count is always greater than or equal to 0, but less than or equal to capacity, as specified in the invariants.
Design by Contract — Release vs Debug:

Being a system to test the correctness of software, it is primarily employed in debug builds of the software and need not be present in the release versions, which has already undergone all the tests.

That means that in a software that is developed using design by contract approach, the debug versions of the software will assert over all the required preconditions, postconditions, and invariants with a clear error report, but this same assertion may not be necessary in the release versions, where we have already tested that all the required contract obligations are always fulfilled. If we remove the assertions and error handling in release builds, we can significantly improve the execution speed of the release build, since it doesn’t have extra code for contract testing which will never be executed at this point.

Question 3

DbC

Answer 3

What is Design by Contract?

Created by Bertrand Meyer in the 1980s, Design by Contract (DbC) is an approach to software design that focuses on specifying contracts that define the interactions among components. DbC is one more tool in our toolkit for gaining confidence that our code is correct, alongside other tools such as type systems, executable test cases, static code analysis, and mutation testing.

An underlying assumption is that components interact with one another in a client-server model. A server makes certain promises (also called obligations) to provide benefits to clients, and client components may assume these promises will be kept. The contract also specifies postconditions and invariants, which participating components must honor.

DbC is based on logical building blocks that existed previously. A key underlying concept is the idea of Hoare triples. In 1969, British computer scientist Tony Hoare proposed that we could reason about the correctness of software by considering how the execution of a section of code changes the state of the computation. The basic formulation is:

{P} C {Q}

where P denotes a precondition, C represents the computation, and Q denotes a postcondition. Preconditions and postconditions are expressed as assertions, in the sense of predicate logic (also known as first-order logic). Those are the basic logical building blocks of DbC.

In DbC, the obligations are preconditions, expressed as assertions; the benefits are postconditions, expressed as assertions; and the invariants are aspects of the system state that are guaranteed not to be affected by the computation.
Eiffel Language

It would have been interesting and useful to define a way of specifying contracts as documentation that programmers could use as a guide for building software based on DbC, but Meyer did not stop there. He also developed a programming language that has DbC constructs built in and enforced at compile time. The Eiffel language implements DbC directly.

To see how DbC can help us, let’s take a look at Eiffel first, as it was the original implementation. Here’s a sample Eiffel class from the DbC intro on the Eiffel site:

class DICTIONARY [ELEMENT]
feature
put (x: ELEMENT; key: STRING) is
– Insert x so that it will be retrievable
– through key.
require
count <= capacity
not key.empty
ensure
has (x)
item (key) = x
count = old count + 1
end

... Interface specifications of other features ...

invariant
0 <= count
count <= capacity
end

The require keyword specifies the preconditions for the put routine in a Dictionary. One or more assertions can follow require. In this example, the preconditions are that the number of dictionary entries (count) doesn’t exceed the capacity of the dictionary, and that the client is not attempting to add an entry that has no key.

The ensure keyword specifies the postconditions for the put routine. It promises that after the put operation, the dictionary will contain the element x, that a lookup based on key will retrieve element x, and that the new count will be one greater than the previous count.

The invariant keyword specifies aspects of the system state that must remain unchanged. The scope of invariant is larger than that of require and ensure, because the invariants must hold true no matter what operations are performed. In the example, the invariants are that the number of items in the dictionary (count) must be positive, and the count cannot exceed the dictionary’s capacity.
Not a Testing Technique

In the course of looking for implementations of DbC for languages other than Eiffel, I noticed a common misconception: Many people think of DbC as a testing technique. The difference between testing and checking is usually clearcut, but the situations in which each can occur may be open to interpretation.

DbC is a form of checking, and it is based on assertions. As Michael Bolton and James Bach put it, “An assertion, in the Computer Science sense, is a kind of check. But not all checks are assertions, and even in the case of assertions, there may be code before the assertion which is part of the check, but not part of the assertion.” DbC is consistent with this observation.

There is also confusion about context; some people assume any sort of check, especially those performed via a software tool, must occur during a “testing phase” of product development or delivery. Issues that I’m seeing with the implementations of DbC libraries may stem from this very misconception. Many DbC solutions are designed to be used during development and testing. They involve “extra” and “optional” libraries that can be enabled and disabled at build time or at runtime. At least one that I looked at requires the code to be compiled with debug options turned on so that the object code is instrumented, and the DbC tool can use debugging information. This would not be done when preparing code for production deployment.

But the intent is that preconditions, postconditions, and invariants are asserted in production with the application running live. That’s the whole point. It’s a hedge against invalid arguments or incorrect data structures being passed into application components; against components inadvertently generating unusable or damaging outputs; against applications changing the system state as an unintended side-effect of their operations. The canonical reference implementation, Eiffel, does not separate DbC checks from the rest of the code. That is not the intent.
Why Not Just Write an “If” Statement?

When you look at various DbC libraries, you discover they tend to be complicated wrappers around relatively basic conditional code. One reason DbC hasn’t caught on in a big way may be that people are intimidated by the apparent complexity of the tools. When investigating the value of DbC, developers often ask, Why not just write an “if” statement for that?

They’re right. The issue isn’t that you couldn’t just write an “if” statement. The problem is that most people don’t bother to write “if” statements. Calling it out as a distinct “thing” with its own name might subtly influence developers to pay more attention to it.

The same Michael Bolton mentioned above tells a story of a time when a developer challenged him to break a web application he had written. The developer was very confident that the code was rock-solid. Bolton not only broke the application, but crashed the server, in a matter of seconds. He pasted the full text of a book from Project Gutenberg into the application’s login form.

So, why didn’t that developer just write an “if” statement? It would have saved him considerable trouble and embarrassment. It’s also arguably a fundamental software engineering competency to guard against well-known security risks. Limiting the size of an input value on a form is pretty basic stuff, after all.
A Thing Becomes Real When It has a Name

Now, maybe if there were a “thing” that software developers could name and discuss (like “Design by Contract,” perhaps), then it would be easier for them to remember to take care of this.

With the growing popularity of microservices, a given application may comprise many small services that are developed independently by people who do not work together and who never meet. Sometimes clients look up services from a registry, and they don’t even know which implementation of a service interface they are calling. These applications live in an inherently insecure environment known as the “Internet.” You may have heard of it.

Some of these clients may even be hostile. Indeed, we know some of them are.

DbC offers a way to ensure code contracts are honored in the wild, when software components may be invoked by client code the service developers know nothing about and do not control. It doesn’t automatically protect against all errors or against determined hackers, but it’s a useful defensive tool.

We cannot manage this situation entirely by checking our code before deployment. We have to manage it actively in production. DbC is meant to enforce the contract for interacting with a component, not merely to check it.

Question 4

JML – Java Modelling Language

Answer 4

formal specification language for sequential Java by
Gary Leavens et. al.
* – to specify behaviour of Java classes & interfaces
* – to record detailed design decisions
* by adding annotations to Java source code in Design-
By-Contract style, using eg. pre/postconditions and
invariants
* Design goal: meant to be usable by any Java
programmer

Question 5

Types of Contracts Supported

Answer 5

• Pre-conditions (requires)
• Post-conditions (ensures)
• Loop Invariants/variants (loop_invariant/ decreases)
• Class Invariants (invariant)

Question 6

In JML class/loop invariants are also in /@ . . . @/

Answer 6

• Class
• invariant formula: Whenever a method is called or returns,
  the invariant has to hold.
• constraint formula: A relation between the pre-state and the
  post-state that has to hold for each method invokation.
• Loop
• loop_invariant formula loop invariant always holds at during
  the iterations of the loop;
• decreases expression It specifies an expression of type long
  or int that must be no less than 0 when the loop is executing,
  and must decrease by a given step each time around the
  loop.