Better Theories in KeY

The loading of key files is not a fun part at all.

1. A special type of file, the logic-datatype files (LDT) are treated specially. The reason is, that these files are always having a Java counterpart, the LDT classes, e.g. SeqLDT. The LDT classes are used to bind the declared logical entities (functions, predicates, etc...) to Java variables. The binding is established after all LDT files have been loaded.

2. We have a global namespace that is cluttered by all theories, and some constructs are defined locally. For example, \schemaVariables are declared local, where \generic G \extends X are declared multiple times globally (and clashes).

3. The loading order is a mess in KeY. Parallel loading is highly unsupported.

4. It is slow! All key files take up to 900 ms.

where problematic rules are

It is a mess!

---

Solution

Make a new more structured theory.

\theory Seq {
  \use    <Theory>; // makes theory known in this scope
  \import <Theory>; // makes all symbols from the theory known in this scope
  \import <Theory> \only <name>, <name>, <name>;
                    // makes only the given symbols known in this scope

  \sorts { ... /* unchanged */ } 

  \datatypes { // to define ADTs 
    List[T] = «a: b, c: d» nil  
            | Cons( T a, List[T] rest );
  }

  \functions { ... /* unchanged */ }
  \predicates { ... /* unchanged */ }
  \axioms { ... /* unchanged */  }
  \rules { ... /* unchanged */  }

  \export nil \as seq_empty; // makes a local (e.g., Seq#nil) globally known as seq_empty

  \binding "classname"; 
}

I suggest following change:

• Syntax: We add a new keyword and command to key files:

  \binding "classname"; 
  

• Semantics: After the loading stages: ground entities (variables, choices, ...), 2nd level (predicate, functions, transformers) and the third level (taclets), the bindings are evaluated.

  Evaluation of a binding means, that the given class (with the given name) is instantiated with the current constructed Services object.

  If the given class is of type LDT, it is added to the list of type converters (LDTs).

  LDTs can be queried by classname to receive an instance.

A better idee:

We introduce a notion of a Theory into KeY.

LDTs are just theories. Why do we not call them so! Proposal points:

2. For each known theory in a folder of KeY files, we generate a Java to access the contents of a theory.

3. Theories span a namespace. To access a symbol from a theory use <thy>#<name>, for example Seq#len.

4. Additionally, we add an \export <thy>#<name> as <name2> which exports a symbol to the global namespace, under a given name.

I really like the idea, I have always wondered why a theory is called LDT in KeY.

In my opinion, your proposal has multiple benefits:

• KeY only needs to load those rules which are needed for the current proof. I think this has potential to speed up loading and probably also proof search, since less rules have to be checked for applicability in proof step.
• The rules would be more organized, which increases readability. We could have a hierarchy (DAG?) of theories (as for example in Isabelle if I am correct), which would also be a first step in understanding and refactoring the currently quite arcane proof search strategy.
• There could maybe also be benefits for the SMT translation: If for example only LIA rules are loaded for a KeY proof, we could set the SMT logic to LIA also, which could help the SMT solver.

regarding 4.: I am not sure about the global namespace and \export. I think I would favor working the other way round using an \import command (on theory level, e.g. \import Seq), to avoid having to write the theory name in front of every function from that theory (not sure how to handle clashes between same function names from different theories though).

I would also vote for introducing a strict separation between axioms and theorems/lemmas, where the latter are enforced to have a proof (i.e. a corresponding proof file in the repo). I think we currently have \axioms and \rules, but there is no real difference between them...

With \export, we can maintain/assemble the good ol' global namespace required too load legacy proofs.