COSC3308
Example of an Operational Semantic. Fall 2013
0. Abstract Program
is-abstract-program = is-statement-list
is-statement-list = is-statement | is-statement-list is-statement
is-statement = is-assignment-statement |
is-if-statement | is-loop-statement |
is-input-statement | is-output-statement
is-assignment-statement = ([s-variable : is-variable],
[s-expression : is-expression])
is-if-statement = ([s-compare : is-compare],
[s-then-clause : is-statement-list],
[s-else-clause : is-statement-list])
is-loop-statement = ([s-compare : is-comparison],
[s-body : is-statement-list])
is-input-statement = ([s-read : is-variable-list])
is-output-statement = ([s-write : is-variable-list])
is-comparison = ([s-left-operand : is-operand],
[s-right-operand : is-operand],
[s-operator : is-comparison-opr])
is-expression = is-integer | is-variable | is-infix-exp
is-infix-exp = ([s-left-operand : is-operand],
[s-right-operand : is-operand],
[s-operator : is-arithmetic-opr])
is-operand = is-integer | is-variable | is-expression
is-comparison-opr = is-LT | is-EQ | is-NE | is-GT
is-arithmetic-opr = is-plus | is-minus | is-multiply
is-variable = ([s-address : is-integer])
1. Syntax
PROG ::= Program Declaration-sequence
begin Statement-sequence end ;
Declaration-sequence ::= Declaration |
Declaration Declaration-sequence
Statement-sequence ::= statement |
Statement statement-sequence
Declaration ::= Identifier-list : Integer ;
Identifier-list ::= Identifier |
Identifier , Identifier-list
Statement ::= Assignment-statement |
If-statement |
Loop-statement |
Input-statement |
Output-statement
Assignment-statement ::= Identifier := Expression ;
If-statement ::= if Comparison then Statement-sequence
endif ; |
if Comparison then Statement-sequence
else Statement-sequence endif ;
Loop-statement ::= While Comparison loop
Statement-sequence endloop ;
Input-statement ::= input Identifier-list ;
Output-statement ::= output identifier-list ;
Comparison ::= ( Operand Comparison-opr Operand )
Expression ::= Factor | Expression + Factor |
Expression - Factor
Factor ::= Operand | Factor * Operand
Operand ::= Integer | Identifier | ( Expression )
Comparison-opr ::= < | = | != | >
Identifier ::= Letter | Identifier Letter |
Identifier Digit
Integer ::= Digit | Integer Digit
Letter ::= A | B | C | D | E | F | G | H | I | J |
K | L | M | N | O | P | Q | R | S | T |
U | V | W | X | Y | Z
Digit ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
2. VDL Semantic definition.
execute-statement-sequence(sequence) =
is<>(sequence) --> Halt
T --> execute-statement-sequence(tail(sequence))
execute-statement(head(sequence))
execute-statement(statement) =
is-assignment-statement(statement) --> execute-assign(statement)
is-if-statement(statement) --> execute-if(statement)
1s-loop-statement(statement) --> execute-loop(statement)
is-input-statement(statement) --> execute-input(statement)
is-output-statement(statement) --> execute-output(statement)
execute-assign(statement) =
store(s-address.s-variable(statement),value)
value: evaluate-expression(s-expression(statement))
execute-if(statement) =
evaluate-comparison(s-compare(statement)) = T -->
execute-statement-sequence(s-then-clause(statement))
T --> execute-statement-sequence(s-else-clause(statement))
execute-loop(statement) =
evaluate-comparison(s-compare(statement)) = T -->
execute-loop(statement)
execute-statement-sequence(s-body(statement))
execute-input(statement) = input(s-read(statement))
execute-output(statement) = output(s-write(statement))
evaluate-expression(expression) =
is-integer(expression) --> PASS: expression
is-variable(expression) --> evaluate-variable(expression)
T --> calculate(left-value,right-value,s-operator(expression))
left-value: evaluate-expression(s-left-operand(expression))
right-value: evaluate-expression(s-right-operand(expression))
evaluate-comparison(comparison) =
compare(left-value,right-value,s-operator(comparison))
left-value: evaluate-expression(s-left-operand(comparison))
right-value: evaluate-expression(s-right-operand(comparison))
calculate(value1,value2,operator) =
is-plus(operator) --> PASS: Value1+value2
is-minus(operator) --> PASS: value1-value2
is-multiply(operator) --> PASS: value1*value2
compare(value1,value2,operator) =
is-LT(operator) & (value1 < value2) --> PASS: T
is-EQ(operator) & (value1 = value2) --> PASS: T
is-NE(operator) & (value1 <> value2) --> PASS: T
is-GT(operator) & (value1 > value2) --> PASS: T
T --> PASS: F
evaluate(variable) =
is-UNDEFINED(elem(s-address(variable))s-storage(Abstract-Machine)))
--> ERROR
T --> PASS:elem(s-address(variable))s-storage(Abstract-Machine))
store(location,value) =
s-storage:MU(s-storage(Abstract-Machine);[elem(location):value])
input(variables) =
is<>(variables) --> Nothing to do
T --> input(tail(variables))
store(s-address(head(variables)),value)
value: input-file
input-file =
is<>(s-input(Abstract-Machine)) --> ERROR
T --> MU(Abstract-Machine: [s-input:tail(s-input(AM))])
output(variables) =
is<>(variables) --> Nothing to do
T --> output(tail(variables)
output-file(value)
value: evaluate-variable(head(variables))
output-file(value) = MU(AM: [s-output: s-output(AM) concat value])