The tool has a brand new visualizer, which includes the following new features:
There is a new user interface, which includes:
A new feature creates diagrammatic meta models from Alloy source. The resulting diagram can be customized with the standard visualization editor.
Subsignatures are now real subtypes. You can specify scopes on subsignatures, and the type checker can detect errors involving a confusion of subsignatures. The type checker can also now detect irrelevances -- errors in which unions, for example, make use of subexpressions that actually have no contribution to the value of the expression as a whole. For example, if File and Dir are subsignatures of FileSystemObject, and contents is a field of Dir, the expression File & Dir will now give a type error (because it always denotes the empty set), and the expression (File + Dir).contents will give a type error because File is irrelevant.
Signatures now have their own namespaces; you can declare fields in two subsignatures of a common signature that have the same name, and they will be disambiguated by context.
Overloading is resolved in a more sophisticated and uniform way, using the entire context of an expression (including arity). For example, if you write the expression x.f & y, the field f can be resolved using the type of y, where previously only the type of x was used. There is no longer a need for a special casting operator $. Instead, on the rare occasion that a field cannot be resolved, you can make a semantics preserving modification of the expression using any of the standard operators, for example writing T <: f to resolve f to the field declared in signature T (using the new domain restriction operator).
Ad hoc unions are permitted. For example, you can declare a singleton signature Null and write an expression such as T + Null for any other signature T. Irrelevant subexpressions of unions are rejected by the type checker.
The separation between semantics and typing is now much cleaner. The semantics of the language is essentially untyped. This should make it easy to understand Alloy. The complications surrounding univ, for example, are gone: univ is simply the set of all atoms in the universe, and can be thought of as a top level signature declared as abstract.
A new scheme called atomization exploits the subtyping to decompose constraints prior to decomposition. This can result in better performance. It also means that expressions that you might think are expensive are in fact no more expensive than their clumsier counterparts in Alloy 2. For example, the expression r.univ denotes the domain of the relation r; in compiling it, the atomization phase will split univ into its subtypes, so that r will actually only be joined with a set of a type that matches its range.
There is now a preferred signature hierarchy, with subsignatures declared using the extends keyword. Subsignatures are by definition disjoint. The keyword abstract on a signature indicates that its subsignatures subsume it. Orthogonal classifications are now declared using the keyword in; subsignatures declared in this way are not mutually disjoint.
The keyword exactly is used in scope specifications to say that there must be exactly some number of atoms in a given signature.
The keywords univ and iden no longer take parameters, and are now defined over the whole universe of atoms. In particular, this means that saying (iden in r) to make a relation r reflexive will normally be too strong; instead you should say (T<: iden in r) where T is the signature in which r is declared. Also, reflexive transitive closure may contain unexpected tuples: for example, if contents is a relation from directories to their contents in a file system model, the expression *contents will also map atoms of other sets (eg, names) to themselves.
The scheme for module poilymorphism has been changed extensively. Polymorphic instantiation is no longer implicit. In Alloy 3, entire modules are parameterized; there are no separately parameterized functions or predicates. When a polymorphic module is opened, signature parameters are supplied. When a component of a module is used, the parameters must also be given, although a component can still be accessed without a module name (and thus without parameters) if unambiguous. An alias can be declared for an opened module to allow shorter references.
The effect of this change is usually to make use of polymorphic modules a bit less succinct, but a lot clearer. The new subtyping system allows modules to be declared that exhibit subtype polymorphism, using univ instead of a type parameter.
A raft of small changes have been made to improve the syntax by making it more uniform and simpler, and to eliminate some features that confused many users.
The keywords univ and iden no longer require parameters. The keyword none always denotes the empty set, so an empty binary relation is written none -> none.
The multiplicity markings, keywords and quantifiers have been brought together. The keyword sole has been replaced with lone. The keywords lone, some and one are used uniformly as quantifiers, multiplicity markings in relations, multiplicity keywords in set declarations and multiplicity keywords on signature declarations. The keywords static and option, and the multiplicity symbols ?, ! and + are gone (although ! is still used for negation).
Multiplicity expressions for relations can now be used in free-standing formulas. A multiplicity formula takes the form expr : multiplicity-expr. For example, you can write name : Person one -> one Name to say that the name relation is one-to-one from Person to Name.
Implicit dereferencing of fields within signature facts has been simplified. Within a signature fact attached to signature S, any field name f declared in S or inherited by S from a supersignature is treated as short for (this.f), unless prefixed by the special marker @. The with keyword is no longer available.
Implicit functions are gone. The keyword fun introduces a function -- a paragraph whose body is an expression. Invoking a function involves simply replacing the invocation by the expression (with arguments instantiated appropriately). The keyword pred introduces a predicate -- a paragraph whose body is a formula. Invoking a predicate gives a formula. The keywords def and result are gone.
The join operator written :: has gone. The receiver syntax invocation x..f(y) is now written x::f(y).
The domain and range restriction operators <: and :>, with the same meaning as in Z, have been added.
Univ and Int are now regarded as signatures declared in the module alloy/lang, which is implicitly imported when needed. This has no effect on how models are written, but it does allow univ and Int to be treated more uniformly in the visualization interface.
The keywords exh and two are gone.
A new keyword has been added so that a model can indicate the number of solutions expected when running a command. Adding to the end of a command the clause expect N says that you expect there to be N solutions. The only effect of this clause is to change how results are reported; its primary use is in regression testing. Currently, the tool only checks whether there is a solution or not, so expect N is equivalent to expect 1 when N is non-zero.
Some new semantic checks have been added to prevent use of features that were not well defined in Alloy 2.
Comprehensions in which the quantified variables are declared to be higher-order (that is, not scalars) are now rejected.
You can learn more about version 3.0 of the Alloy language with the Tutorial, the Reference Manual, and the FAQ.