Properties such as associativity may be attributed to functions.Some properties of (binary) functions are particularly significant for tools. For instance, associativity may be relevant when parsing specifications that use infix notation: repeated applications may be left ungrouped, since all possible groupings are semantically equivalent. Associativity, commutativity, idempotence, and unit properties may also be significant for term-rewriting tools.
Attributions of properties such as associativity to functions are familiar from (e.g.) OBJ3, where they are specified together with function declarations. CASL allows this too. It was also tentatively proposed to allow attributions to be specified as separate items, so that further properties might be attributed to previously-declared functions in extensions of specifications; but this can be achieved in CASL by simply redeclaring the function(s), now with the desired attribution(s). Providing attributions as separate items would also permit the concise attribution of the same properties to an arbitrary list of functions, possibly having different profiles, but it seems that such a feature would be of limited use in practice.
Attributions are distinct from axioms.Properties like associativity may also be asserted using axioms. For conciseness, such axioms could also be specified generically, and instantiated for particular sorts and functions. Tools, however, need to be able to distinguish attributions from general axioms, which motivates CASL providing a separate construct for them.