Formal specs.

Writing is nature’s way of letting you know how sloppy your thinking (reasoning) is.

A specification is a written description of what (not how) a function, a module or a system is supposed to do.

What exactly a function or a module should do, not how. Irrelevant details have to be abstracted out.

Specifying a function or a module helps us understand it at a higher level of concepts or abstractions.

Concepts and relations among them is a level of abstraction above the code. It corresponds to how we think.

it’s a good idea to write a specification of a function or a module before implementing it. Nothing clarifies the mind better than writing thoughts down.

Writting formally, using standard notiaions, eliminates ambiguity and imprecision of a human language.

The tools are TLA+, and sometimes Agda or Idris.

The actual data representation and an implementation of an algorithm

• the how - has to be encapsulated and hidden behind a /public

interface/, which constitutes an abstraction barrier, inside a module which implements an Abstract Data Type.

This is how a hierarchical, and layered sub-systems is to be build, the way Nature does.

Functions or modules are “cells”, signatures or interfaces are “membranes”.

Protocols are contracts, which correspond to a phisical constraints of a shared environment. A network is a shared environment.

Our basic tool for writing specifications is mathematics.

Mathematics is nature’s way of letting you know how sloppy your writing is.

Formal mathematics is nature’s way of letting you know how sloppy your mathematics is

Logicians have developed ways of eliminating mere words and making the mathematics completely formal and, hence, completely precise.

It’s hard to be clear and precise in an imprecise and ambigous language like English.

To avoid errors, science and engineering have adopted mathematics as their language

Each equation is a precise assertion after being proven to be correct.

Most specifications require only simple application of a few standard mathematical concepts (Numbers, Sets and Sequences).

Mathematics is a set of formal domain-specific languages to describe the Universe (particular aspects of reality).

The Set Theory and First-Order Logic are the most fundamental DSLs.

The language of Sets could be thought of as an embedded DLS for logic. Or an extension.

the generalized and abstracted out the notion of a Number and operations on them).

write down a mathematical model of an aspect of reality.

specify what we expect of a program and do so formally in a mathematical language.

so that we could effectively prove the equivalence of the two and verify their equivalence by computer.

Meaning is a mathematical model Semantics, denotational semantics

Write specs in Haskell, not abstract math

Specification is a mathematical model

• Adequate (captures, abstracts out correctly)
• Simple (straightforward, simplest structures)
• Precise (proof of adequacy and self-fool-proof)

try to write our code to pack as much of the proof into the type system as possible.

think of the code as a black box about which all we can see is its surface: its specification.

A specification is written for humans to read, not machines. (formal specifications, at least invariants checking in TLA+)

“Specs” can take time to write well, and it is time well spent.

The main goal is clarity. It is also important to be concise.

A well-written specification usually has several parts communicating different kinds of information about the thing specified.

Definitional (declarative) specifications instead of operational (imperative).

write simple, slow implementations first, then improve bottlenecks as necessary.

The specification forms an abstraction barrier that protects the implementer from the client and vice versa.

Locality is one of the benefits of abstraction by specification. A module can be understood without needing to examine its implementation.

it promotes loose coupling between different code modules. If one module changes, other modules are less likely to have to change to match.

The client should not assume more about the implementation than is given in the spec because that allows the implementation to change.

Making assumptions about the implementation that are not guaranteed by the specification is known as violating the abstraction barrier.

Reading and writing specifications requires close attention to detail.

A specification is a contract between a client of some unit of code and the implementer of that code.

As soon as a design decision is made, document it in a specification.

The most common place we find specifications is as comments in the interface (.mli) files for a module.

So, specifications are informal (formal are in TLA).

There, the implementer of the module spells out what the client may and may not assume about the module’s behavior.

Specifications usually involve preconditions and postconditions.

The preconditions inform what the client must guarantee about inputs they pass in, and what the implementer may assume about those inputs.

The postconditions inform what they client may assume about outputs they receive, and what the implementer must guarantee about those outputs.

Those are informally specified constraints on inputs and outputs.

An implementation satisfies a specification if it provides the behavior described by the specification.

There may be many possible implementations of a given specification that are feasible.

• preconditions (constraints on inputs)
• exceptions (when, if any)
• boundary cases (empty containers, etc)
• postconditions (the type of the range)

Specifications should be written quite early.

Specifications should continue to be updated throughout implementation.

a template Returns: (range, postconditions) Requires: (domain, preconditions) Raises: Example: (use/call side)