104 Constraint-Violating Updates
Predica has one kind of constraint boundary: a transaction boundary. Every constraint applicable to transaction-controlled database state is required to hold at that boundary. A program that produces a constraint-violating database state there is illegal. A compiler should reject as many such illegal programs as it can prove will, or may, produce a violation at a transaction boundary.
This legality rule is independent of constraint-checking strategy. The language does not require an implementation to check constraints at runtime and does not prescribe an exception, trap, rollback, continuation, or other behaviour when an undetected violation occurs. An implementation may insert checks in a debug or checked build and omit them in another build.
The transaction boundary
Construction, assignment, procedure calls, function returns, collection insertion, and other ordinary program operations are not constraint boundaries. Completing a constructor is not a constraint boundary. Constraints are not required to hold merely because a value is fully initialised, read, passed, returned, captured, or otherwise made available to program code.
An update transaction begins from committed database state and may pass through any number of intermediate states that violate constraints. The several coordinated updates required to restore consistency need not be expressed as one statement. Constraints are required to hold again only at the transaction boundary.
Program values and constructors
Constraints are not required to hold for ordinary program variables or for values held in them. A program may construct, read, pass, return, capture, and update a fully initialised local value whose declared constraints are false. Such a value may later be changed into one satisfying the constraints, or may never be written to transaction-controlled database state at all.
Constructor syntax is only a convenience for initialising a value. It does not check constraints or create a point at which they are required to hold. The same value may instead be built by declaring a variable and initialising its constituent locations programmatically. The definite-initialisation rules still apply independently of constraints; see Uninitialised Locations.
Transaction state
The individual database-state updates inside a transaction are not constraint boundaries. Intermediate transaction states may violate constraints. At the transaction boundary, the resulting database state must satisfy all constraints applicable to that data partition.
A program that attempts to commit a constraint-violating final state is illegal. The language does not prescribe whether the implementation detects the violation, rejects the commit, reports an exception, traps, or exhibits some other behaviour. A database or transaction API may provide additional checked-operation guarantees, but those guarantees are library or implementation contracts rather than consequences of the Predica language semantics.
Kinds of constraint
Constraint-violation legality is distinct from the static formation rules of the language:
- an expression or update with incompatible element types is rejected statically;
- a statically provable cardinality incompatibility is rejected statically;
- a possible read of an uninitialised location is rejected statically;
- the definite-initialisation rules govern when locations may be read;
- nominal, relational, key, cardinality, and other declared constraints on database state are required to hold at transaction boundaries.
An implementation may use static reasoning, generated checks, database validation, or any combination of them to diagnose illegal programs. These techniques do not change which programs are legal.