%------------------------------------------------------------------------------
% 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
%------------------------------------------------------------------------------
am[V:TYPE+]: THEORY
BEGIN
IMPORTING Cont[V], Instruction[V], State[V], list_props_aux
Stack: TYPE+ = list[int]
Config: TYPE+ = [Code,Stack,State]
c,c0,c1,c2: VAR Code
e,e0,e1,e2: VAR Stack
s,s0,s1,s2: VAR State
n,n0,n1,n2,k,k1,k2: VAR nat
pn: VAR posnat
cf,cf0,cf1,cf2: VAR Config
i: VAR int
x: VAR V
f1: VAR [int->int]
f2: VAR [[int,int]->int]
check1(c,e,s):bool = NOT null?(e)
check2(c,e,s):bool = (NOT null?(e)) AND (NOT null?(cdr(e)))
push(i,e): Stack = cons(i,e)
pop(e:(cons?[int])):Stack = cdr(e)
top(e:(cons?[int])):int = car(e)
step(c,e,s): Config
= IF null?(c) THEN (c,e,s) ELSE
CASES car(c) OF
PUSH(i) : (cdr(c),push(i,e),s),
FETCH(x) : (cdr(c),push(s(x),e),s),
UNARY(f1) : IF check1(c,e,s)
THEN (cdr(c),push(f1(top(e)),pop(e)),s)
ELSE (c,e,s) ENDIF,
BINARY(f2) : IF check2(c,e,s)
THEN (cdr(c),push(f2(top(e),top(pop(e))),pop(pop(e))),s)
ELSE (c,e,s) ENDIF,
STORE(x) : IF check1(c,e,s)
THEN (cdr(c),pop(e),assign(x,top(e))(s))
ELSE (c,e,s) ENDIF,
NOOP : (cdr(c),e,s),
BRANCH(c1,c2): IF check1(c,e,s)
THEN IF top(e) = 1
THEN (append(c1,cdr(c)),pop(e),s)
ELSE (append(c2,cdr(c)),pop(e),s) ENDIF
ELSE (c,e,s) ENDIF,
LOOP(c1,c2) : (append(c1,
cons(BRANCH(append(c2,cons(LOOP(c1,c2),null)),
cons(NOOP,null)),cdr(c))),e,s)
ENDCASES ENDIF
tr(n)(cf0,cf): RECURSIVE bool
= IF n=0 THEN cf0=cf
ELSE (NOT null?(cf0`1)) AND
cf0 /= step(cf0) AND
tr(n-1)(step(cf0),cf) ENDIF
MEASURE n
step_append: LEMMA NOT null?(c1) AND
(append(c1,c2),e,s) /= step((append(c1,c2),e,s)) =>
(c1,e,s) /= step((c1,e,s))
tr_add: LEMMA tr(k1+k2)(cf0,cf2) IFF
EXISTS cf1: tr(k1)(cf0,cf1) AND tr(k2)(cf1,cf2)
tr_eq: LEMMA tr(k)(cf0,cf1) AND tr(k)(cf0,cf2) => cf1 = cf2
code_partial: LEMMA % N&N 3.4
tr(k)((c0,e0,s0),(c1,e1,s1)) =>
tr(k)((append(c0,c2),append(e0,e2),s0), (append(c1,c2),append(e1,e2),s1))
code_split: LEMMA % N&N 3.5
tr(k)((append(c1,c2),e,s),(null,e2,s2)) =>
EXISTS e1,s1,k1,k2: tr(k1)((c1,e,s),(null,e1,s1)) AND
tr(k2)((c2,e1,s1),(null,e2,s2)) AND
k1+k2=k
IMPORTING Cont
M(c):Cont
= lambda s:
IF EXISTS n,s1: tr(n)((c,null,s),(null,null,s1))
THEN up(choose({s1 | EXISTS n: tr(n)((c,null,s),(null,null,s1))}))
ELSE bottom ENDIF
M_deterministic: LEMMA M(c)(s) = up(s1) IFF % N&N 3.6
EXISTS n: tr(n)((c,null,s),(null,null,s1))
END am
¤ Dauer der Verarbeitung: 0.19 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
