Userdefined abstract data types¶
Abstract
KeY allows you to define abstract data types and use them inside the logic and JML specifications.
Introduction¶
Abstract data types comes in many favours. Often we think on ADTs as the typical algebraic data type defined by the its constructor, e.g., a simple list is defined by
type 'a List = Nil  Cons(a, List)
in Ocaml. But Abstract Data Types are wider category, it also contains coinductive or nongenerated data types. Let us model a set inside of KeY. Of course, a set can be modelled using a list and an uniqueness constraint on the list elements, but this model would not be able to reflect infinite sets such as natural numbers or all possible objects. Such data types are defined coinductive, which comes in an opaque sort, and obeserver functions upon them.
KeY supports both.
Algebraic Data Types (before KeY2.14.0)¶
You need to split your Algebraic Data Type into a sort and (constructor) functions. For example, a list would be defined as
\sorts { List; }
\functions{ \unique List Nil; \unique List Cons(any,List); }
Cons(1, Cons(2, Nil))
for the list \langle 1,2 \rangle. To reason about the list, you normally need to define an induction scheme. In KeY you declare a Taclet:
\rules {
\schemaVariables {
\schemavar List list;
\schemavar formula fml;
}
induction_on_list {
\varcond( \notFreeIn(list, fml) )
"Nil Case" : \add( ==> {\subst fml; Nil} fml );
"Cons(any,List) Case" :
\add( ==>
( \forall List l; {\subst list; l} fml )
> ( \forall List tail; \forall any ele; {\subst list; Cons(ele,tail)} fml )
);
"Use Case" : \add( \forall List l; {\subst list; l} fml ==> );
};
}
The Taclet induction_on_list
corresponds to the rule:
A complete example can be found in the KeY repo, in standard_key/adt/list.key
Algebraic Data Types (with KeY2.14.0 and beyond)¶
Since version 2.14.0, the KeY grammar supports the direct notation of algebraic data types. The grammar for ADTs follows the typical syntax in KeY combined with functional language. ADTs are defined within a \datatypes { ... }
block, and are translated onto the existing infrastructure (Sorts, Functions, Taclets). The grammar is as follows:
\datatypes {
<name> = <constructor>  ...  <constructor>;
...
}
<cname>( <sort> <argName>, ...)
with named arguments. From a datatype definition, we derive the following logical entities for the signature, on the example of a list \datatypes { List = Nil  Cons(any element, List tail); }
:
 a sort named after the ADT name, e.g., here it would be
List
.  a function for each constructor which takes arguments of the constructor and evaluates to the ADT.
Here, we would have:
\functions{ List Nil(); List Cons(any,List); }
 Three taclets for the use in reasoning on the ADT structure.

Axiom taclets that adds the induction principle as an axiom on the sequence. $$ \frac{ (\forall a \in ADT.~ \phi) \leftrightarrow \phi[a/c_1] \wedge \ldots \wedge \phi[a/c_n] \Longrightarrow }{ \forall a \in ADT.~ \phi[a] } $$

Induction taclets for proving a sentence for all ADTs. (Like the induction rule above.) $$ \frac{ \begin{matrix} \forall a \in ADT; \phi \Longrightarrow \ \Longrightarrow \phi[a/c_1] \ \Longrightarrow \ldots \ \Longrightarrow phi[a/c_n] \end{matrix} }{ \Longrightarrow \forall a \in ADT.~ \phi[a] } $$
This taclet is a direct consequence of the induction formula.

A case distinction taclet, which allows you to split a proof attempt along the possible different values of an ADT.
This is a direct consequence of the disjunction x = c_1 \vee\ldots\vee x = c_n resulting from the construction principles of ADTs. This is valid for generated ADTs where the values can only be constructed using the constructors. This allows us to make a case distinction about the various constructors.
Following our example we obtain the following taclets:
List_Axiom {
\schemaVar \formula phi;
\schemaVar \variables List x;
\find(\forall x; phi)
\varcond(\notFreeIn(x, phi))
\add(
\forall x; phi
<> {\subst x;Nil}phi
& \forall List tail; \forall any head; ({\subst x;tail}phi > {\subst x;Cons(head, tail)}phi)
==>
)
\displayname "Axiom for List"
}
List_Ind {
\schemaVar \formula phi;
"Nil": \add(==> {\subst x;Nil}phi);
"Cons(anyhead,Listtail)":
\add(
==>
\forall tail; \forall head; ({\subst x;tail}phi > {\subst x;Cons(head, tail)}phi)
);
"Use case of List":
\add(\forall x; phi ==>)
\displayname "Induction for List"
}
List_ctor_split {
\schemaVar \term MyList var;
\schemaVar \skolemTerm any head;
\schemaVar \skolemTerm MyList tail;
\find(var)
\sameUpdateLevel
"#var = Nil": \add(var = Nil ==>);
"#var = Cons": \add(var = Cons(head, tail) ==>)
\displayname "case distinction of List"
}
Coinductive Data Types¶
Coinductive types are also possible in KeY. For example, the builtin sorts Heap
and LocSet
are coinductive. There is no direct syntactical support for these datatypes.
Using a Data Type in JML¶
You can use any sort of the logical signature in JML. For this, you need the prefix the sort name with the \dl_
to access the JavaDL scope. Some sorts are also direct builtin into JML, like \map
, and are direct reachable.
A typical pattern is to have a ghost variable, that represents the current state of a class by using logical datatype and uninterpreted functions.
public class MyMap {
//@ public ghost \map logical_dt;
public void put(Object k, Object v) {
//@ set logical_dt = \dl_map_put(logical_dt, k, v);
...
}
}
Instead of \map
you can also use \dl_map
which points to the same sort.