Quelle  Instruction.pvs

%------------------------------------------------------------------------------
% An Instruction Set for an Abstract Machine for while
%
% All references are to HR and F Nielson "Semantics with Applications:
% A Formal Introduction", John Wiley & Sons, 1992. (revised edition
% available: http://www.daimi.au.dk/~hrn )
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
%     Version 1.0            25/12/07  Initial Version
%------------------------------------------------------------------------------

Instruction[V:TYPE+]: THEORY

BEGIN

  Instruction: DATATYPE
  BEGIN
    PUSH(n:int)                     : PUSH?
    FETCH(x1:V)                     : FETCH?
    UNARY(f1:[int->int])            : UNARY?
    BINARY(f2:[[int,int]->int])     : BINARY?
    STORE(x2:V)                     : STORE?
    NOOP                            : NOOP?
    BRANCH(c1,c2:list[Instruction]) : BRANCH?
    LOOP(c3,c4:list[Instruction])   : LOOP?
  END Instruction

  Code: TYPE+ = list[Instruction] CONTAINING null

  i,j: VAR int

  PUSH_TRUE:  MACRO Instruction = PUSH(b2n(TRUE))
  PUSH_FALSE: MACRO Instruction = PUSH(b2n(FALSE))
  ADD:   MACRO Instruction = BINARY(lambda i,j: i+j)
  SUB:   MACRO Instruction = BINARY(lambda i,j: i-j)
  MUL:   MACRO Instruction = BINARY(lambda i,j: i*j)
  EQ:    MACRO Instruction = BINARY(lambda i,j: b2n(i=j))
  LE:    MACRO Instruction = BINARY(lambda i,j: b2n(i<=j))
  NEG:   MACRO Instruction = UNARY(lambda i: 1-i)
  B_AND: MACRO Instruction = MUL

END Instruction