164 Annotator

The Predica annotator is a source-to-source analysis tool. It loads Predica files, resolves and type-checks them in their component context, and writes annotated Predica files that preserve the same source-tree structure. The annotated files are still Predica source files; generated annotations are comments inserted next to the source items they explain.

This chapter describes the annotator, not any particular command-line interface. The interface used to choose input components, include roots, output folders, or diagnostic policy is outside this chapter.

Mirrored source output

Given a set of loaded Predica source files, the annotator produces a corresponding set of output files with the same relative paths and filenames. Authors write ordinary Predica source, not a special annotation-only form. The ordinary source text, comments, declaration order, formatting, and folder layout are preserved; generated annotation comments are the differences.

An annotation is attached to the source item whose denotation it describes by placing one or more line comments immediately before that item. The indentation of the comment follows the indentation of the annotated item. Long annotations wrap over several line comments. 


// area=(W * H):Real
// where
//   this.width(W) ∧ this.height(H)
→ Real area = width * height;

When the annotator has no current translation for a particular source item, it preserves the copied source file and attaches a local skipped annotation with the reason. Unsupported denotations are visible at the source item they explain. 


// denotation skipped: no denotation rule for fold prototype
→ Real prototypeStatus = supplier.status.Σprototype;

What is annotated

The annotator is not limited to top-level query examples. It annotates Predica code in general wherever a useful source item has a value, logic, or location denotation. This includes:

  • schema constraints, including constraints written in constraints blocks and constraints attached to attributes;
  • derived attributes and other derived variables whose value is defined by an expression;
  • query or expression statements used as examples;
  • update statements, where the left-hand side has a location denotation and the right-hand side has a value denotation.

The presentation varies with the source item. A query expression is annotated with its value denotation. A constraint is annotated with the closed formula that the constraint contributes to schema validity. An assignment is annotated by relating its target-location denotation to the right-hand value denotation.

Constraint annotations

For a constraint expression C declared on a type T, the annotator uses the same constraint rule as the query-frame semantics. It translates C in an environment where this denotes the constrained value of type T. If the translation produces one Boolean result term B, the annotation is the closed formula: 


∀vars(free(γ_C)) ( formula(γ_C) → B )

This is a universal formula over the values reached while evaluating the constraint. A constraint such as age ≥ 18 on Person does not mean that there exists an age greater than or equal to 18; it means every age value of the person satisfies the predicate. 


entity Person
{
    Integer age;

    constraints
    {
        // ∀A:Integer (this.age(A) → A ≥ 18)
        age ≥ 18;
    }
}

Boolean-valued path expressions are handled the same way. The path contributes the predicates needed to reach the Boolean value, and the Boolean value becomes the consequent of the implication. 


entity FirearmLicence
{
    Boolean valid;
}

entity FirearmPurchase
{
    FirearmLicence licence;

    constraints
    {
        // ∀V:Boolean ∀L:FirearmLicence (
        //   this.licence(L) ∧ L.valid(V) → V)
        licence.valid;
    }
}

The names chosen for generated logic variables are not semantically significant. Alpha-equivalent annotations express the same constraint.

Derived attribute and variable annotations

A derived attribute is a member whose value is computed from an expression rather than stored as a base attribute. The same treatment applies to any derived variable declaration whose right-hand side has a value denotation.

For a derived member a on type T, the right-hand expression is translated with this:T in scope. If the expression produces one result, the annotation is relabelled with the declared member name and declared type of a. This makes the comment describe the source declaration being annotated, not merely the anonymous result of the right-hand expression. 


value Rectangle
{
    Real width;
    Real height;

    // area=(W * H):Real
    // where
    //   this.width(W) ∧ this.height(H)
    → Real area = width * height;
}

Derived path declarations expose the path formula that defines the derived member. 


entity Course {}

entity Enrolment
{
    Student student;
    Course course;
}

entity Student
{
    Enrolment enrolment* where enrolment.student = this;

    // enrolled=C:Course
    // where
    //   ∃E:Enrolment (this.enrolment(E) ∧ E.course(C))
    → Course enrolled* = enrolment.course;
}

When a derived declaration is inherited, specialised, or produced by a generic instantiation, the default annotation remains close to the source declaration the user wrote. Debug views show instantiated forms, but the ordinary annotation of a generic source declaration is parametric rather than a list of unrelated monomorphic copies.

Statement and update annotations

The annotator also explains program statements. For an assignment, the left-hand side is interpreted as a location expression and the right-hand side as a value expression, both in the statement pre-state. The annotation makes both denotations visible enough to explain what is being written. 


// target:
//   status=AttrLoc(S, Supplier.status):Integer
//   where s.supplier(S) ∧ S.city("London")
// value:
//   5:Integer
s.supplier.[city = "London"].status := 5;

The target part is a location denotation: it identifies the selected attribute slots, not the value currently stored in those slots. The value part is the ordinary value denotation of the right-hand expression. For compound update operators, the annotation also indicates the read-modify-write expression being applied when that is not obvious from the source operator.

Inlining and normalisation policy

Annotations are denotations in logic. The annotator may simplify expressions and formulas, remove redundant quantifiers, rename generated variables, use compact names, wrap lines, and pretty-print.

Generated annotations preserve ordinary fold abstraction. Named folds such as Σsum, Σcount, Σmean, and user-defined folds such as Σmedian render as fold applications over their input comprehension, for example Σcount({ ... }):Integer.

The resolved standard logical folds std.exists, std.empty, std.all, and std.any render as logical formulas in every annotation context. Boolean value annotations may therefore be formulas.

For an input comprehension 


C = { V:T for F where Ψ }

the logical readings before simplification are: 


C.Σexists  ↦  ∃vars(F) Ψ
C.Σempty   ↦  ¬∃vars(F) Ψ
C.Σall     ↦  ∀vars(F) (Ψ → V)      // V:Boolean
C.Σany     ↦  ∃vars(F) (Ψ ∧ V)      // V:Boolean

The final comment is rendered after simplification and pretty-printing. For example, C.Σempty may render as ∀vars(F) ¬Ψ, which is equivalent to ¬∃vars(F) Ψ.

All other folds use Σop(C) fold-application rendering. 


// total=Σsum({ S:Integer where this.status(S) }):Integer
→ Integer total = status.Σsum;

// ∀S:Integer (this.status(S) → S > 0)
status.(this > 0).Σall;