-------------------------------------- | While semantics expressed in Alloy | | | | Jason Reich | | jr523@cs.york.ac.uk | -------------------------------------- : While.als : Central alloy file. Implements the execution 'trace' of 'SmallSteps'. : WhileExpressions.als : Implements While arithmetic and boolean expressions, states and variables. Evaluates expressions based on execution state. : WhileStatements.als : Implements While abstract syntax and control-flow semantics. Determines, given conditions, what the next statement to be executed is. : While.thm, WhileStatements.thm : Themes to use in visualiser when displaying the relevant submodels models. Need a lot of work. : While2Alloy/ : Java program to convert a While program into Alloy clauses suitable for this model. Requires CUP parser runtime <http://www2.cs.tum.edu/projects/cup/> to compile. CUP and JFlex used to generate Tokenizer / Parser. ECLIPSE project. : w2a.jar : Fat JAR file of While2Alloy. Ready to execute. Run using "java -jar w2a.jar <while file>". Will output Alloy to stdout. Ready to be used in predicates or run commands. VERY UNFORGIVING. Useless error messages. Early version. N.B. While statements are lower case. Variables are single character upper case. E.g. [[ if (X == 10) then skip else X := 10 ]] : test.while, test2.while : Example programs that do work in the w2a translator.