41 Construction Project Example

This example shows how legality conditions can be expressed directly as constraints across a small network of related entities:

• Multi-entity legality: legality depends on the builder, licence, zoning rule, environmental clearance, project site and recorded violations.
• Temporal constraints: the licence and environmental clearance must be valid at the project start date.
• Identity and backlink constraints: licences, clearances and violations must refer to the same builder, site or project being certified.
• Cross-value constraints: project height and intended use must be compatible with the zoning rule.
• Declarative legality: there is no procedural validation code, only constraints that describe compliant worlds.

entity Person
{
    String name;
    Integer age;
}

entity BuilderLicence
{
    Person holder;
    Date validFrom;
    Date validTo;
    Boolean suspended;

    constraints
    {
        // ∀A:Integer ∀H:Person
        //     (this.holder(H) ∧ H.age(A) → A ≥ 18)
        holder.age ≥ 18;

        // ∀V:Date ∀V1:Date
        //     (this.validFrom(V) ∧ this.validTo(V1) → V ≤ V1)
        validFrom ≤ validTo;
    }
}

entity ZoningRule
{
    String zone;
    Integer maxHeight;
    Boolean residential;
    Boolean commercial;
}

entity EnvironmentalClearance
{
    String siteId;
    Boolean approved;
    Date expiry;
}

entity ConstructionProject
{
    String id;
    String siteId;
    Person builder;
    BuilderLicence licence;
    ZoningRule zone;
    Boolean residential;
    Boolean commercial;
    Integer height;
    EnvironmentalClearance clearance;
    Date startDate;

    constraints
    {
        // 1. Builder must match the licence holder
        // ∀H:Person ∀B:Person ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.holder(H) ∧ this.builder(B) → H = B)
        licence.holder = builder;

        // 2. Licence must be valid at the start date
        // ∀V:Date ∀S:Date ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.validFrom(V) ∧ this.startDate(S) → V ≤ S)
        licence.validFrom ≤ startDate;

        // ∀S:Date ∀V:Date ∀L:BuilderLicence
        //     (this.startDate(S) ∧ this.licence(L) ∧ L.validTo(V) → S ≤ V)
        startDate ≤ licence.validTo;

        // 3. Licence must not be suspended
        // ∀S:Boolean ∀L:BuilderLicence
        //     (this.licence(L) ∧ L.suspended(S) → ¬S)
        ¬licence.suspended;

        // 4. Height must comply with zoning
        // ∀H:Integer ∀M:Integer ∀Z:ZoningRule
        //     (this.height(H) ∧ this.zone(Z) ∧ Z.maxHeight(M) → H ≤ M)
        height ≤ zone.maxHeight;

        // 5. Environmental clearance must be approved and valid
        // ∀A:Boolean ∀C:EnvironmentalClearance
        //     (this.clearance(C) ∧ C.approved(A) → A)
        clearance.approved;

        // ∀S:Date ∀E:Date ∀C:EnvironmentalClearance
        //     (this.startDate(S) ∧ this.clearance(C) ∧ C.expiry(E) → S ≤ E)
        startDate ≤ clearance.expiry;

        // 6. The clearance must be for this project site
        // ∀S:String ∀S1:String ∀C:EnvironmentalClearance
        //     (this.clearance(C) ∧ C.siteId(S) ∧ this.siteId(S1) → S = S1)
        clearance.siteId = siteId;

        // 7. Residential/commercial compatibility
        //    (example: a commercial project cannot be built in a residential-only zone)
        // ∀R:Boolean ∀R1:Boolean ∀Z:ZoningRule
        //     (this.residential(R) ∧ this.zone(Z) ∧ Z.residential(R1) ∧ R → R1)
        residential → zone.residential;

        // ∀C:Boolean ∀C1:Boolean ∀Z:ZoningRule
        //     (this.commercial(C) ∧ this.zone(Z) ∧ Z.commercial(C1) ∧ C → C1)
        commercial → zone.commercial;

        // ∀R:Boolean ∀C:Boolean
        //     (this.residential(R) ∧ this.commercial(C) → ¬(R ∧ C))
        ¬(residential ∧ commercial);
    }
}

entity Violation
{
    ConstructionProject project;
    String code;
    Boolean resolved;
}

entity LegalProject
{
    ConstructionProject project;
    Violation violation*;

    constraints
    {
        // All violations must be resolved
        // ∀R:Boolean ∀V:Violation
        //     (this.violation(V) ∧ V.resolved(R) → R)
        violation.resolved;

        // Every listed violation must belong to this legal project
        // ∀P:ConstructionProject ∀P1:ConstructionProject ∀V:Violation
        //     (this.violation(V) ∧ V.project(P) ∧ this.project(P1) → P = P1)
        violation.project = project;
    }
}