| products/sources/formale Sprachen/PVS/while/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Instruction.pvs Sprache: PVSOriginal von: 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 ¤ Dauer der Verarbeitung: 0.17 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
