FMSE
Formal
Methods in
Software Engineering
Tools K-3.5.1 Anonymous  Login

This tool is intended to bring out the flavour of the K framework (version 3.5.1) by offering a web interface for the following features: compile a K definition for a programming language and use it for running programs written in that language. The user can run directly or modify the existing definitions and programs in order to experiment the tool. Note that any modification of a file has to be saved (using Save button) before usage.

Compiling a language definition: select the .k file the you want to kompile from the file tree in the left hand side and then hit the Kompile button.

Example: compiling tutorial/1_k/2_imp/lesson_4/imp.k

Step 1: select tutorial/1_k/2_imp/lesson_4/imp.k 

Step 2: press Kompile and wait for compilation to finish

Step 3: check if the folder tutorial/1_k/2_imp/lesson_4/imp-kompiled is generated; otherwise the compilation is not successful

 

Running a program: select a program from the left hand side file tree and hit the KRun button. Note that you also have to specify the compiled definition (see example below).

Example: running tutorial/1_k/2_imp/lesson_1/tests/sum.imp

Step 1: select tutorial/1_k/2_imp/lesson_1/tests/sum.imp 

Step 2: specify the compiled definition; assume that we want to run this program using the definition we compiled above, and for this, in Params text field, we add -d ../../lesson_4/ .

The -d option is followed by the relative path to the folder containing the compiled definition.

Step 3: check the result 

Note: in the Params text field one can insert any option available from command line. Therefore, one can also insert --help to see all the available options either for Kompile or Krun.


Examples
Loading ...
Path : 

Input
     Params:
   StdIN:
  

Output:
@FMSE 2010-2011