On contracts and implementations

["G.B." <rm-dash-bau-haus@dash.futureapps.de>]

There is a claim that contracts of Ada 2012 are part of the
implementation. They are not.

Assuming that they are part of the implementation is a misconception
about designing with contracts.

The contract idea is, rather, to make engineers not program
defensively, but to agree on a contract that states what is
true. The word "Contract" as we know it: to call the post-hoc
conditions of a program's state a "contract" would be a misnomer.

Technically, contracts can be evaluated on separate hardware #2,
controlling hardware #1. The following program is an example.

"Subtract a non-negative number from a non-negative number"

P0:     LOAD    Input, R1
         LOAD    Input, R2
         $TRNSFR #2
         BLT     R1, 0, [T1]
         BLT     R2, 0, [T1]
         BGE     R1, 0, [P1]
T1:     $STOP   #1
         $STOP   #2
P1:     $TRNSFR #1
         SUB     R2, R1, R0

Hardware #2 gets a copy of the register words of #1, and a read-only
copy of the program and its memory.

Then, the program that harware #1 runs, is, essentially,

P0:     LOAD    Input, R1
         LOAD    Input, R2
         SUB     R2, R1, R0

This is efficient, since defensive checking is gone: once the program
has been shown to be correct, $TRNSFR may mean to just skip the tests.

As always, if engineers decide to plant side effects into predicates,
they are on their own.

Sorry for the steam, but it is perhaps a good idea to state that it is
the engineers who take responsibility for writing proper contracts,
and then using them.