CS422 - HW5 information

From FSL
Jump to: navigation, search

Advice: Start this homework early, because this is your first time you use K-Maude. Since K-Maude is an experimental tool, please feel free to report any issues you have with it even if you are not sure whether they are bugs in the tool or your own misunderstanding. Both Traian (tserban2) and myself (grosu) are here to help you, just ask. Good luck!

Obtaining K-Maude

Please check the K-framework project page at http://k-framework.googlecode.com/ . The sources for K-Maude can be retrieved by following the instructions from Source->Checkout (direct link: http://code.google.com/p/k-framework/source/checkout ).

Existing definitions

The languages defined so far using the K framework can be found in the examples directory (including SIMPLE). The directory simple contains 2 subdirectories, untyped containing the definition of the untyped version of the language, and typed which in turn contains three subdirectories: static, for the static semantics, i.e., the type checker, dynamic, for the dynamically typed version of SIMPLE, and dynamic-typed-locations which is a variant of dynamic, in which the type information is maintained in the environment.

Please update regularly using "svn up" from the base directory to benefit of the latest fixes and features.

Writing definitions

When writing new definitions: all definitions should load the k-prelude.maude file, and the semantics should include the K module. The name of the main module of a definition should be the capitalized version of the name of the file containing it.

When adding new rules to a definition, keep in mind the following important restrictions:

  • Never define two operations with the same name, and
  • Any operation should be applied on terms of sorts lower than those declared in the arity (that is, no subterm appearing in the definition should parse to a kind; if desired, overload the operations to extend their range).

Compiling definitions

To compile a definition: execute the kcompile.sh script passing as parameter the name of the file containing the main module. If the compilation succeeds, the output would be placed in name-of-the-file-compiled.maude . Currently, the script only runs under Unix.

Recommendations on running the script:

  • The Maude executable should be on the path and MAUDE_LIB should point to the location where prelude.maude resides
  • The script should be run from the directory where the definition resides, e.g., by providing the relative path to the script. The scrips should not be moved from the tools directory.

Example of usage: from the examples/simple/untyped directory run the script as:

MAUDE_LIB=<maudeDir> ../../../tools/kcompile.sh simple-untyped.maude

where <maudeDir> should be replaced by the path where prelude.maude reside Alternatively, you could set MAUDE_LIB in your .bash_profile and add the tools directory to the path, and run the script as:

 kcompile.sh simple-untyped.maude

Testing definitions

The definitions of the various semantics for SIMPLE provided in the K-Maude distribution contain a very simple testing functionality, provided in the main module of the definition. These simple tests consists from the definition of a constant run, which creates an initial configuration for a program and an input. For all definitions, the chosen program is pSorting, and for the dynamic semantics, it includes an input. If you would like to test other programs, feel free to modify the definition of run and then recompile. Once the compilation is completed, one just needs to load in Maude the compiled version of the definition and then test is by running

 rew run .

Case study: compiling simple-untyped on a csil (or other 64bit linux) machine

Below is a sequence of actions that, if performed in order, should get the untyped version of simple compiled.

Note: you don't have to perform the steps below exactly as specified. This is just a sample of something that should work.

wget http://maude.cs.uiuc.edu/download/current/maude-linux64.tar.gz
tar -xzf maude-linux64.tar.gz
  • Rename the executable maude.linux64 into maude (alternatively, you could edit the script or create a symbolic link)
mv maude-linux64/maude.linux64 maude-linux64/maude
  • Check out K
svn checkout http://k-framework.googlecode.com/svn/trunk/ k-framework
  • Go to the directory where your definition resides
cd k-framework/examples/simple/untyped
  • Run kcompile script with the file containing your definition as argument
bash -c "PATH=~/maude-linux64:~/k-framework/tools:$PATH MAUDE_LIB=~/maude-linux64 kcompile.sh simple-untyped"
  • Load your compiled definition inside Maude
bash -c "PATH=~/maude-linux64:$PATH MAUDE_LIB=~/maude-linux64 maude simple-untyped-compiled"
  • Once inside Maude, try rewriting "run":
Maude> rew run .

You should see a large configuration, with everything in the compiled form. Look for the k cell to be empty < k > .K </ k >, usually meaning that the program has finished executing and the output cell to have some reasonable output.

Personal tools