config.tex

\chapter{Configuration}
K is a framework that is used to define formal specifications of programming languages. The K framework is designed to easily correspond to a finite automaton. In a different programming language, it is much harder to represent the program as a formal model because it would require modeling many different parts of the machine. K, on the other hand, can directly compile to Isabelle proofs and be verified. The rules in K are already mathematically precise due to being written in K.

However, code written in K is also executable. It can run example programs using the formal semantics written in it. This means that the K code can run test sets for validation. K code can be considered validated if it passes all the standard test suites provided for a compiler or an interpreter, for example.

A configuration of an automaton is the definition of the specific structure that contains all code and memory that the automaton contains and operates on.

K is used for defining a state machine and the K rules define the transition rules for the state machine. The configuration of the state machine is made up of K cells. The K cells contain the syntax data structure representing the code of the example program. They also contain the memory of the state machine. An actual state of the state machine in K is when the cells each have some term inside of them.

Syntax for a programming language can be written in K using the constructor \texttt{syntax} while semantic rules are written in K using the constructor \texttt{rule}.

K rules can be used to edit the program code as well as edit the other cells that make up the program state.

In the description below I give incrementally the various components that make up the configuration used in the Haskell static semantics given in this paper, along with a brief description of what they name and examples of what they hold and how they are used.

\noindent
The cells are defined using XML syntax.

\begin{lstlisting}
requires "haskell-syntax.k"

module HASKELL-CONFIGURATION
    imports HASKELL-SYNTAX

    syntax KItem ::= "startImportRecursion"
    syntax KItem ::= callInit(K)

    configuration 
        <T>
            <k> $PGM:ModuleList ~> startImportRecursion </k>
            <tempModule> .K </tempModule>
            <tempCode> .K </tempCode>
\end{lstlisting}

\noindent
The \texttt{$<k>$} cell is the cell that computation takes place in.
The abstract syntax tree is initially placed into the \texttt{$<k>$} cell.

\noindent
The command

\begin{lstlisting}
$PGM:ModuleList
\end{lstlisting}

\noindent
means that the parsed tree appears in this cell and the sort that contains all other sorts is \texttt{ModuleList}.

\noindent
Putting \texttt{$.K$} means that the cell is initially empty.

\noindent
The name of the current module is \texttt{tempModule}. The current code is \texttt{tempCode}.

\noindent
The cell \texttt{typeIterator} is used for creating a fresh type variable for the inference algorithm. It has the current count of how many fresh type variables were created.

\begin{lstlisting}
            <typeIterator> 1 </typeIterator>
\end{lstlisting}

\section{Alpha}
The data structure \texttt{Alpha} is a map of type renamings. More is explained in Chapter 5.

So if a user declares

\begin{lstlisting}
data MyBool = TTrue
;type MyBooltwo = MyBool
\end{lstlisting}

\noindent
then \texttt{MyBooltwo} is a renaming of \texttt{MyBool}. In \texttt{tempAlpha}, an \texttt{AObject} is made. An \texttt{AObject} is a \texttt{KItem} with two children. One can be thought of as a Key and the other is the Value for a map. So \texttt{MyBooltwo} is an alias for \texttt{MyBool} and \texttt{MyBooltwo $->$ MyBool} in the map. However, we want to check and reject programs that have the same name as an alias for multiple types, so the semantics does not initially use a K Map which has idempotence. However, once it makes this check, it then switches to using a K Map. This is what \texttt{tempAlphaMap} is.

\texttt{.Map} means that the cell starts with an empty map.

\begin{lstlisting}
            <tempAlpha> .K </tempAlpha>
            <tempAlphaMap> .Map </tempAlphaMap>
\end{lstlisting}

\section{Beta}

\texttt{tempT} contains all user-defined data types. \texttt{tempT} is organized in such a way that makes context-sensitive checks easy to perform. \texttt{tempBeta} contains all user-defined data types organized so that type inference is easy to perform. More is explained in Chapter 5.
\begin{lstlisting}
            <tempBeta> .Map </tempBeta>
            <tempT> .K </tempT>
\end{lstlisting}

\subsection{Example}
If the user makes the data type \texttt{CusBool} in module \texttt{Simp5}, and declares it with this example:
\begin{lstlisting}
	data CusBool = True2 | False2
\end{lstlisting}

\noindent
then the corresponding \texttt{tempBeta} should look as below. Note how the monomorphic datatype just has an empty \texttt{forAll} and \texttt{TyVars}. For more on monomorphic and polymorphic types, see Chapter 5.

\begin{lstlisting}
    <tempBeta>
        ModPlusType ( Simp5 , False2 ) |-> forAll ( .Set , CusBool .TyVars )
        ModPlusType ( Simp5 , True2 ) |-> forAll ( .Set , CusBool .TyVars )
    </tempBeta>
\end{lstlisting}

If the user makes the data type \texttt{CusBool} in module \texttt{Simp5}, and declares it with the example
\begin{lstlisting}
data CusBool a b = True2 a | False2 b
\end{lstlisting}

\noindent
then the corresponding \texttt{tempBeta} should look like this:
\begin{lstlisting}
    <tempBeta>
        ModPlusType ( Simp5 , False2 ) |-> forAll ( a b , funtype ( b , CusBool a b ) )
        ModPlusType ( Simp5 , True2 ) |-> forAll ( a b , funtype ( a , CusBool a b ) )
    </tempBeta>

\end{lstlisting}

\section{Delta}

\texttt{tempDelta} contains the arity of the user-defined data types. So if a user-defined data type takes in two parameters, \texttt{tempDelta} will contain a mapping from the module and the data type name to the number 2. Again, it is initially empty.

\begin{lstlisting}
            <tempDelta> .Map </tempDelta>
\end{lstlisting}

\subsection{Example}
If the user makes the data type \texttt{CusBool} in module \texttt{Simp5}, and declares it with the example
\begin{lstlisting}
data CusBool a b = True2 a | False2 b
\end{lstlisting}

\noindent
then the corresponding \texttt{tempDelta} should look like this:

\begin{lstlisting}
<tempDelta>
     ModPlusType ( Simp5 , CusBool ) |-> 2
</tempDelta>
\end{lstlisting}

\section{Import Data Structure}

\texttt{importTree}, \texttt{recurImportTree}, and \texttt{impTreeVMap} contain the data necessary for the directed acyclic graph representing imports.

\begin{lstlisting}
            <importTree> .List </importTree>
            <recurImportTree> .List </recurImportTree>
            <impTreeVMap> .Map </impTreeVMap>
\end{lstlisting}

More is explained in Chapter 6.

\section{Modules}

The modules cell contains all modules that were checked and inferred already. Multiplicity means that there can be multiple module cells.

\begin{lstlisting}
            <modules> //static information about a module
                <module multiplicity="*">
                    <moduleName> .K </moduleName>
                    <moduleAlphaStar> .K </moduleAlphaStar>
                    <moduleBetaStar> .K </moduleBetaStar>
                    <moduleImpAlphas> .List </moduleImpAlphas>
                    <moduleImpBetas> .List </moduleImpBetas>
                    <moduleCompCode> .K </moduleCompCode>
                    <moduleTempCode> .K </moduleTempCode>
                    <imports> .Set </imports>
                    <classes> //static information about a module
                        <class multiplicity="*">
                            <className> .K </className>
                        </class>
                    </classes>
                </module>
            </modules>
        </T>

endmodule
\end{lstlisting}

The components here are the module specific versions of the ones just discussed.