10 Database Values and Consistency

A Predica schema defines the type of a database. A database state is a value of that type, and a database is a variable whose successive values are database states. For example:

entity ShipmentsSystem
{
    Supplier supplier*;
    Part part*;
    Shipment shipment*;
}

var db = openDatabase<ShipmentsSystem>("/path/to/database");

Here ShipmentsSystem is a nominal entity type, db is a database variable of that type, and the current value of db is a complete database state. Expressions such as db.supplier designate pseudovariables within that state.

Consistency as type membership

A constraint is part of a nominal type and restricts the values belonging to that type. If S is the unconstrained structural carrier of a database type and K is the conjunction of its applicable constraints, then the carrier of the constrained database type is:

carrier(S with K) =
{
    d ∈ carrier(S)
    |
    K(d)
}

A database state is consistent if and only if it belongs to this constrained carrier. Consistency is therefore type membership at the level of the complete database value. The applicable constraints include attribute types, attribute cardinalities, keys, derived definitions, where clauses, subtype structure, and explicit constraint blocks.

This account does not require consistency to be checked one relvar at a time. A constraint may relate several predicate extensions in the same database value. The database type defines which combinations of extensions constitute valid states.

Consistency and correctness

Consistency is not the same as correctness. A database can satisfy every declared constraint while containing a false statement about the modelled world. For example, a database might consistently record that a supplier is located in Paris even though the supplier is actually located in London. The constraints determine which database values are admissible; they do not establish that the base facts supplied to the database are true.

In Predica's descriptive interpretation, constraints classify admissible models. In its normative interpretation, they classify compliant worlds. In either interpretation, consistency means satisfaction of the specification. Whether the specification itself accurately expresses the intended domain is a separate question.

Consistency and satisfiability

Checking a database value is also different from checking the specification itself. For a particular structural database value d, consistency asks whether K(d) holds. Satisfiability asks whether any such value exists:

∃d ∈ carrier(S). K(d)

If this formula is false, the constrained carrier is empty. The type definition is meaningful, but no database state can inhabit it. A consistency check can reject one proposed state; a satisfiability check detects that every proposed state must be rejected.

Transactions preserve consistency

An update transaction begins with a consistent database state and constructs a proposed successor state. Individual update statements may pass through intermediate transaction states that violate constraints. The transaction boundary is the point at which the complete proposed state is required to satisfy the applicable constraints.

committed update : ShipmentsSystem -> ShipmentsSystem

The notation above states the semantic contract rather than the implementation strategy. A legal successful commit replaces one value of the database type with another. A program that attempts to commit a proposed final state outside the constrained carrier is illegal; the language does not prescribe the runtime behaviour of that attempt. See Constraint-Violating Updates.

This leaves implementations free to use mutation, logs, snapshots, copy-on-write pages, or other physical techniques. Those techniques do not change the logical account: the externally committed states are values of the declared database type.

Local and global constraints

Good schema design makes many consistency conditions follow compositionally from type definitions, keys, cardinalities, and correctly placed attributes. A constraint that initially appears global may indicate that a domain is missing or that a fact has been attached to the wrong subject. Normalisation uses dependencies as diagnostics for finding such designs.

Some business rules genuinely relate several independently meaningful predicate extensions. Such a rule remains an explicit constraint on the database type. It still contributes to the definition of the constrained carrier, but it is not thereby local to an individual attribute or entity type. The distinction between local structure and explicit global constraints remains important even though both participate in determining consistency.