The Acme Predicate Language
The Acme predicate language is the portion of the Acme design language used for specifying the predicates of design invariants and design heuristics. The predicate language is based on first-order predicate logic with composable terms, user-definable functions, and limited quantification capabilities. To keep the language decidable, variables may be quantified only over finite sets.
This chapter presents the core constructs of the predicate language in four sections: primitive functions, operators, quantification, and design analyses. Each of these sections provides a description of the construct, examples of its use, and a semi-formal description of its syntax and semantics.
The semantics given for the predicate logic language are less formal than those given for the Acme structural and type languages because the predicate language consists primarily of predicate logic expressions, which is a well understood semantic domain in and of itself. As such, discussion of language construct semantics focuses on the portions of the predicate language that differ from traditional predicate logic, or require a tricky integration with the rest of the Acme language. For primitive functions and operators a simple intuitive description of the item’s meaning should suffice. Tricky semantic issues, on the other hand, include how to evaluate a predicate expression in the semantic domain (e.g. for determining type satisfaction), how parameters are passed to functions, and the scope and visibility of identifiers in expressions. These issues are dealt with in Chapter 3’s detailed discussion of the semantics of the type system.