You will be implementing one global operation, Next_Primitive_Instruction, that determines the next primitive instruction to be executed in a compiled BL program. Working with your partner and before closed lab, carefully read the (informal) specifications provided below and then design and code the body of Next_Primitive_Instruction. In implementing Next_Primitive_Instruction, you should use the other two operations provided, Evaluate_Jump_Condition and Is_Primitive_Instruction_Code, but you do not need to implement them (code for these operations will be provided in closed-lab). Review your code carefully and trace it on some examples. The objective is to have code that works the first time you type it in (except perhaps for typos).
///-------------------------------------------------------------
/// Local Context ----------------------------------------------
///-------------------------------------------------------------
enumeration What_A_Bug_Can_See_In_Front_Of_It
{
EMPTY,
WALL,
FRIEND,
ENEMY
};
///-------------------------------------------------------------
enumeration Instruction_Code
{
MOVE,
TURNLEFT,
TURNRIGHT,
INFECT,
SKIP,
HALT,
JUMP,
JUMP_IF_NOT_NEXT_IS_EMPTY,
JUMP_IF_NOT_NEXT_IS_NOT_EMPTY,
JUMP_IF_NOT_NEXT_IS_WALL,
JUMP_IF_NOT_NEXT_IS_NOT_WALL,
JUMP_IF_NOT_NEXT_IS_FRIEND,
JUMP_IF_NOT_NEXT_IS_NOT_FRIEND,
JUMP_IF_NOT_NEXT_IS_ENEMY,
JUMP_IF_NOT_NEXT_IS_NOT_ENEMY,
JUMP_IF_NOT_RANDOM,
JUMP_IF_NOT_TRUE
};
///-------------------------------------------------------------
concrete_instance
class Compiled_Program :
instantiates
Array_Kernel_1 <Integer>
{};
// Note: A compiled BL program is just a sequence of integer
// instruction codes stored in an array of integers.
///-------------------------------------------------------------
/// Global operations ------------------------------------------
///-------------------------------------------------------------
global_function Boolean Evaluate_Jump_Condition (
preserves Integer what_bug_sees,
preserves Integer jump_instr
);
/*!
requires
[what_bug_sees is in What_A_Bug_Can_See_In_Front_Of_It and
jump_instr is one of the conditional jump
instructions in Instruction_Code]
ensures
[Assume jump_instr = JUMP_IF_NOT_condition.
Evaluate_Jump_Condition returns true if and only if
condition is true given what_bug_sees.]
!*/
//--------------------------------------------------------------
global_function Boolean Is_Primitive_Instruction_Code (
preserves Integer instr
);
/*!
ensures
Is_Primitive_Instruction_Code =
(instr = MOVE) or (instr = TURNLEFT) or
(instr = TURNRIGHT) or (instr = INFECT) or
(instr = SKIP) or (instr = HALT)
!*/
//--------------------------------------------------------------
global_procedure Next_Primitive_Instruction (
preserves Compiled_Program& prog,
preserves Integer what_bug_sees,
alters Integer& pc,
produces Integer& primitive_instruction
);
/*!
requires
[prog is a valid BugsWorld virtual machine program and
what_bug_sees is in What_A_Bug_Can_See_In_Front_Of_It and
0 <= pc <= prog.ub]
ensures
[Returns in primitive_instruction the next primitive
instruction (MOVE, TURNLEFT, TURNRIGHT, INFECT, SKIP,
or HALT) that should be executed in program prog given
what_bug_sees and starting execution at location #pc
in prog. pc is the location in prog immediately after
the location in prog of primitive_instruction.]
!*/
//--------------------------------------------------------------