Formal Semantics

The Appendix A of the Fortress 1.0 beta language specification includes the following Fortress calculi:

  • Basic Core Fortress

Basic Core Fortress allows only a small subset of the Fortress language to be formalized. Basic Core Fortress includes trait and object definitions, method and field invocations, and self expressions. The types of Basic Core Fortress include type variables, instantiated traits, instantiated objects, and the distinguished trait Ob ject. Among other features, Basic Core Fortress does not include top-level variable and function definitions, overloading, excludes clauses, bounds clauses, where clauses, object expressions, and function expressions.

  • Core Fortress with Where Clauses

Core Fortress with Where Clauses is a straightforward extension of Basic Core Fortress. An object or trait definition may include where clauses. Every method invocation is annotated with three kinds of static types by type inference: the static types of the receiver, the arguments, and the result. These type annotations appear in Core Fortress with Where Clauses in a form of "as τ". If the annotated types are not enough (to find “witnesses” for the where-clauses variables), type checking rejects the program and requires more type information from the programmer. Section 11.6 of the Fortress specification describes where clauses.

  • Core Fortress with Overloading

Core Fortress with Overloading is a straightforward extension of Basic Core Fortress. It includes top-level function definitions and provides overloading for dotted methods and first-order functions. Chapters 15 and 33 describe Fortress overloading.

  • Acyclic Core Fortress with Field Definitions

Core Fortress with Overloading is a straightforward extension of Basic Core Fortress. It includes field definitions inside object definitions and provides acyclic type hierarchy of Fortress.

You are more than welcome to contribute any core calculus with any Fortress language feature to the Fortress formalism work! Contributions are solicited in (but not limited to) the following:

  • Core Fortress with Excludes and Comprises Clauses (Section 9.1)
  • Core Fortress with Coercion (Chapters 17 and 33)
  • Core Fortress with Operator and Identifier Parameters (Section 11.5)
  • Core Fortress with Nat, Int, and Bool Parameters (Sections 11.2 and 11.3)
  • Core Fortress with Dimensions and Units (Chapters 18 and 35)