7 Further Developments

It is indeed suitable to enlarge the class of CASL programs that can be executed with ELAN. A few extensions are underway:

• Structured specifications: ELAN is also a modular language with an importation mechanism. The CASL construct

  SPEC1 and ... and SPECn then { ... }
  

  corresponds to the ELAN importation construct:

  import global SPEC1 ... SPECn ; end
  

• Mixfix operators are both allowed in CASL and ELAN syntax. The translation should be easy to adapt. One can also think to allow more attributes for operators.
• For now, we require to mention in the program the sort of each axiom. This information could be computed at parsing time.

Boyond these relatively easy extensions, there are also challenging questions: for instance, how to integrate ELAN labelled rules and strategies into CASL? How to deal with the specification of non-deterministic functions in CASL? In ELAN, non determinism is allowd since a computation can have a multiset of results (i.e. of normal forms). We could describe such specifications by introducing multiset operations to handle multisets of results, as done for instance in [Bor98]. In this case of course, execution of specifications with associative and commutative functions (like multiset union) is of prime interest.