| Quellcodebibliothek Statistik Leitseite products/sources/formale Sprachen/PVS/ints/ (Beweissystem Isabelle Version 2025-1©) Datei vom 28.9.2014 mit Größe 1 kB |
|
Quelle Instruction.pvs Sprache: 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.20 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28