CS计算机代考程序代写 flex syntax

syntax
Data-Stack Theory
stack all stacks of items of type X
empty a stack containing no items
push a function that takes a stack and an item and gives back another stack pop a function that takes a stack and gives back another stack
top a function that takes a stack and gives back an item
1/51

axioms
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
Data-Stack Theory
empty→s1→s2→s3→s4
↑
|
2/51

axioms
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
Data-Stack Theory
empty→s1→s2→s3→s4
|
↑
3/51

axioms
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
push s x = push t y = s=t ∧ x=y
Data-Stack Theory
empty→s1→s2→s3→s4→………. ……….→t→u→v→w→……….
4/51

axioms
Data-Stack Theory
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
push s x = push t y = s=t ∧ x=y empty, push stack X: stack
empty, push B X: B ⇒ stack: B
empty→s1→s2→s3→s4→……….
5/51

axioms
Data-Stack Theory
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
push s x = push t y = s=t ∧ x=y empty, push stack X: stack
empty, push B X: B ⇒ stack: B
P empty ∧ ∀s: stack· ∀x: X· Ps ⇒ P(push s x) =
∀s: stack· Ps
6/51

axioms
Data-Stack Theory
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
push s x = push t y = s=t ∧ x=y empty, push stack X: stack
empty, push B X: B ⇒ stack: B
P empty ∧ ∀s: stack· ∀x: X· Ps ⇒ P(push s x) =
pop (push s x) = s top (push s x) = x
∀s: stack· Ps
7/51

implementation
stack = empty = push = pop = top =
[*int]
[nil]
〈s: stack → 〈x: int → s;;[x]〉〉
〈s: stack → if s=empty then empty else s [0;..#s–1] fi〉 〈s: stack → if s=empty then 0 else s (#s–1) fi〉
Data-Stack Theory
8/51

Data-Stack Theory
proof
Prove that the axioms of the theory are satisfied by the definitions of the implementation.
(the axioms of the theory) ⇐ (the definitions of the implementation) specification ⇐ implementation
9/51

Data-Stack Theory
proof (last axiom):
top (push s x) = x
= top (〈s: stack → 〈x: int → s;;[x]〉〉 s x) = x
= top (s;;[x]) = x
= 〈s: stack → if s=empty then 0 else s (#s–1) fi〉 (s;;[x]) = x
= if s;;[x]=empty then 0 else (s;;[x]) (#(s;;[x])–1) fi = x
= if s;;[x]=[nil] then 0 else (s;;[x]) (#(s;;[x])–1) fi = x
= (s;;[x]) (#s) = x
= x = x =⊤
definition of push
apply function definition of top apply function definition of empty simplify the if and the index index the list reflexive law
10/51

usage
var a, b: stack
a:= empty. b:= push a 2
consistent?
yes, we implemented it.
complete?
no, the binary expressions pop empty = empty top empty = 0
are unclassified. Proof: implement twice.
Data-Stack Theory
11/51

Theory as Firewall
user ensures that ⎥ ⎥ implementer ensures that only stack properties ⎥ theory ⎥ all stack properties
are relied upon ⎥ ⎥ are provided
12/51

axioms
Simple Data-Stack Theory
empty: stack
push: stack→X→stack pop: stack→stack
top: stack→X
push s x ⧧ empty
push s x = push t y = empty, push stack X: stack
empty, push B X: B ⇒ stack: B
P empty ∧ ∀s: stack· ∀x: X· Ps ⇒ P(push s x) =
pop (push s x) = s top (push s x) = x
stack ⧧ null
s=t ∧ x=y
∀s: stack· Ps
13/51

Data-Queue Theory
emptyq: queue join q x: queue join q x ⧧ emptyq
join q x = join r y = q=r ∧ x=y q⧧emptyq ⇒ leave q: queue
q⧧emptyq ⇒ front q: X
emptyq, join B X: B ⇒ queue: B
leave (join emptyq x) = emptyq
q⧧emptyq ⇒ leave (join q x) = join (leave q) x) front (join emptyq x) = x
q⧧emptyq ⇒ front (join q x) = front q
14/51

Strong Data-Tree Theory
emptree: tree
graft: tree→X→tree→tree emptree, graft B X B: B ⇒ tree: B graft t x u ⧧ emptree
grafttxu=graftvyw = t=v∧x=y∧u=w left (graft t x u) = t
root (graft t x u) = x right (graft t x u) = u
15/51

tree ⧧ null
graft t x u: tree
left (graft t x u) = t root (graft t x u) = x right (graft t x u) = u
Weak Data-Tree Theory
16/51

Data-Tree Implementation
tree = emptree, graft tree int tree
emptree = [nil]
graft = 〈t:tree→〈x:int→〈u:tree→[t;x;u]〉〉〉 left = 〈t:tree→t0〉
right = 〈t:tree→t2〉
root = 〈t:tree→t1〉
17/51

Data-Tree Implementation
[[[nil]; 2; [[nil]; 5; [nil]]]; 3; [[nil]; 7; [nil]]]
[;3;] [;2;] [;7;] [nil] [ ;5; ] [nil] [nil]
[ nil ] [ nil ]
18/51

Data-Tree Implementation
tree = emptree, graft tree int tree
emptree = 0
graft = 〈t: tree → 〈x: int → 〈u: tree → “left”→t | “root”→x | “right”→u〉〉〉 left = 〈t: tree → t “left”〉
right = 〈t: tree → t “right”〉
root = 〈t: tree → t “root”〉
19/51

“left” →
(“left” → 0
| “root” → 2
| “right” → (“left” → 0
| “root” → 5
| “right” → 0 ) )
(“left” → 0
| “root” → 7
| “right” → 0 )
| “root” → 3 | “right” →
Data-Tree Implementation
20/51

data theory
s:= push s x
program theory
push x
user’s variables, implementer’s variables
Theory Design
21/51

syntax
axioms
push pop top
topʹ=x ⇐
ok ⇐ push x. pop
a procedure with parameter of type X a program
expression of type X
ok
⇐ push x. pop
= push x. ok. pop
⇐ push x. push y. pop. pop
Program-Stack Theory
push x
22/51

syntax
axioms
push pop top
topʹ=x ⇐
ok ⇐ push x. pop
a procedure with parameter of type X a program
expression of type X
topʹ=x
⇐ push x. ok
⇐ push x. push y. push z. pop. pop
Program-Stack Theory
push x
23/51

Program-Stack Implementation
var s: [*X] implementer’s variable
push = pop = top =
〈x: X → s:= s;;[x]〉 s:= s [0;..#s–1]
s (#s–1)
Proof (first axiom):
( topʹ=x ⇐ push x )
= ( sʹ(#sʹ–1)=x ⇐ s:= s;;[x] )
= ( sʹ(#sʹ–1)=x ⇐ sʹ = s;;[x] ) =⊤
consistent? yes, implemented.
complete? no, we can prove very little if we start with pop
definitions of push and top rewrite assignment with one variable List Theory
24/51

Fancy Program-Stack Theory
topʹ=x ∧ ¬isemptyʹ ⇐ push x ok ⇐ push x. pop
isemptyʹ ⇐ mkempty
25/51

Weak Program-Stack Theory
topʹ=x ⇐ push x
topʹ=top ⇐ balance
balance ⇐ ok
balance ⇐ push x. balance. pop
countʹ = 0 ⇐ start
countʹ = count+1 ⇐ push x countʹ = count+1 ⇐ pop
26/51

Program-Queue Theory
isemptyqʹ ⇐ mkemptyq
isemptyq ⇒ frontʹ=x ∧ ¬isemptyqʹ ⇐ join x ¬isemptyq ⇒ frontʹ=front ∧ ¬isemptyqʹ ⇐ join x
isemptyq ⇒ (join x. leave = mkemptyq) ¬isemptyq ⇒ (join x. leave = leave. join x)
27/51

Program-Tree Theory
Variable node tells the value of the item where you are. node:= 3
Variable aim tells what direction you are facing.
aim:= up aim:= left aim:= right
Program go moves you to the next node in the direction you are facing, and turns you facing back the way you came.
Auxiliary specification work says do anything, but
do not go from this node (your location at the start of work )
in this direction (the value of variable aim at the start of work ). End where you started, facing the way you were facing at the start.
28/51

Program-Tree Theory
(aim=up) = (aimʹ⧧up) ⇐ go
nodeʹ=node ∧ aimʹ=aim ⇐ go. work. go
work ⇐ ok
work ⇐ node:= x
work ⇐ a=aim⧧b ∧ (aim:= b. go. work. go. aim:= a) work ⇐ work. work
29/51

Data Transformation
user’s variables u implementer’s variables v
new implementer’s variables w
data transformer D relates v and w such that ∀w· ∃v· D specification S is transformed to ∀v· D ⇒ ∃vʹ· Dʹ ∧ S
v S vʹ
D Dʹ w ∀v· D ⇒ ∃vʹ· Dʹ ∧ S wʹ
30/51

example
Data Transformation
user’s variable u: bin implementer’s variable v: nat operations
zero = v:= 0 increase = v:= v+1 inquire = u:= even v
new implementer’s variable w: bin data transformer w = even v
31/51

Data Transformation
∀v·D ⇒ ∃vʹ·Dʹ ∧ zero
= ∀v· w = even v ⇒ ∃vʹ· wʹ = even vʹ ∧
= ∀v· w = even v ⇒ ∃vʹ· wʹ = even vʹ ∧ uʹ=u ∧ vʹ=0
= ∀v· w = even v ⇒ wʹ = even 0 ∧ uʹ=u
= ∀r: even nat· w=r ⇒ wʹ=⊤ ∧ uʹ=u
= wʹ=⊤ ∧ uʹ=u
= w:= ⊤
(v:= 0)
1-pt change variable 1-pt
32/51

Data Transformation
∀v· D ⇒ ∃vʹ· Dʹ ∧ increase
= ∀v· w = even v ⇒
= ∀v· w = even v ⇒
= ∀v· w = even v ⇒
= ∀r: even nat· w=r ⇒ wʹ = ¬r ∧ uʹ=u
= wʹ=¬w ∧ uʹ=u
= w:= ¬w
(v:= v+1)
∃vʹ· wʹ = even vʹ ∧ ∃vʹ· wʹ = even vʹ ∧ wʹ = even (v+1) ∧
uʹ=u uʹ=u
∧
vʹ=v+1
1-pt change var 1-pt
33/51

Data Transformation
∀v· D ⇒ ∃vʹ· Dʹ ∧ inquire
= ∀v· w = even v ⇒ ∃vʹ· wʹ = even vʹ ∧ (u:= even v)
= ∀v· w = even v ⇒ ∃vʹ· wʹ = even vʹ ∧ uʹ = even v ∧ vʹ=v
= ∀v· w = even v ⇒ wʹ = even v ∧ uʹ = even v
= ∀r: even nat· w=r ⇒ wʹ=r ∧ uʹ=r
= wʹ=w ∧ uʹ=w
= u:= w
1-pt change var 1-pt
34/51

example
Data Transformation
user’s variable u: bin implementer’s variable v: bin operations
set = v:=⊤ flip = v:=¬v ask = u:=v
new implementer’s variable w: nat data transformer v = even w
35/51

Data Transformation
∀v·D ⇒ ∃vʹ·Dʹ ∧ set
= ∀v· v = even w ⇒ ∃vʹ· vʹ = even wʹ ∧ (v:= ⊤)
= even wʹ ∧ uʹ=u
⇐ w:= 0
36/51

Data Transformation
∀v·D ⇒ ∃vʹ·Dʹ ∧ flip
= ∀v· v = even w ⇒ ∃vʹ· vʹ = even wʹ ∧ (v:= ¬v)
= even wʹ ⧧ even w ∧ uʹ=u
⇐ w:= w+1
37/51

Data Transformation
∀v·D ⇒ ∃vʹ·Dʹ ∧ ask
= ∀v· v = even w ⇒ ∃vʹ· vʹ = even wʹ ∧ (u:= v)
= even wʹ = even w = uʹ
⇐ u:= even w
38/51

Security Switch
A security switch has three binary user’s variables a , b , and c . The users assign values to a and b as input to the switch. The switch’s output is assigned to c . The output changes when both inputs have changed. More precisely, the output changes when both inputs differ from what they were the previous time the output changed. The idea is that one user might flip their input indicating a desire for the output to change, but the output does not change until the other
user flips their input indicating agreement that the output should change. changes back before the second user changes, the output does not change.
binary implementer’s variables
A records the state of input a at last output change B records the state of input b at last output change
If the first user
39/51

Security Switch
A security switch has three binary user’s variables a , b , and c . The users assign values to a and b as input to the switch. The switch’s output is assigned to c . The output changes when both inputs have changed. More precisely, the output changes when both inputs differ from what they were the previous time the output changed. The idea is that one user might flip their input indicating a desire for the output to change, but the output does not change until the other
user flips their input indicating agreement that the output should change. changes back before the second user changes, the output does not change.
operations
a:=¬a. ifa⧧A∧b⧧Bthenc:=¬c. A:=a. B:=belseokfi b:=¬b. ifa⧧A∧b⧧Bthenc:=¬c. A:=a. B:=belseokfi
If the first user
40/51

replace old implementer’s variables A and B with nothing!
data transformer
A=B=c
proof
Security Switch
∃A, B· A=B=c ⇐⊤
operations
a:=¬a. ifa⧧A∧b⧧Bthenc:=¬c. A:=a. B:=belseokfi b:=¬b. ifa⧧A∧b⧧Bthenc:=¬c. A:=a. B:=belseokfi
generalization, using c for both A and B
41/51

Security Switch
∀A, B· A=B=c ⇒ ∃Aʹ, Bʹ· Aʹ=Bʹ=cʹ ∧ ifa⧧A∧b⧧Bthenc:=¬c. A:=a. B:=b else ok fi
expand assignments, dependent compositions, and ok = ∀A, B· A=B=c ⇒ ∃Aʹ, Bʹ· Aʹ=Bʹ=cʹ ∧ if a⧧A ∧ b⧧B
then aʹ=a ∧ bʹ=b ∧ cʹ=¬c ∧ Aʹ=a ∧ Bʹ=b
else aʹ=a ∧ bʹ=b ∧ cʹ=c ∧ Aʹ=A ∧ Bʹ=B fi
use one-point law for A and B , and for Aʹ and Bʹ
= if a⧧c ∧ b⧧c then aʹ=a ∧ bʹ=b ∧ cʹ=¬c ∧ cʹ=a ∧ cʹ=b else aʹ=a ∧ bʹ=b ∧ cʹ=c ∧ cʹ=c ∧ cʹ=c fi
= if a⧧c ∧ b⧧c then aʹ=a ∧ bʹ=b ∧ cʹ=¬c ∧ cʹ=¬c ∧ cʹ=¬c else aʹ=a ∧ bʹ=b ∧ cʹ=c ∧ cʹ=c ∧ cʹ=c fi
= ifa⧧c∧b⧧cthenc:=¬celseokfi
= c:= (a⧧c ∧ b⧧c) ⧧ c
use context
42/51

user’s variables: c: bin and x: X
old implementer’s variables: Q: [n*X] and p: nat operations
mkemptyq = p:= 0
isemptyq = c:= p=0
isfullq = c:= p=n
join = Qp:= x. p:= p+1
leave = for i:= 1;..p do Q(i–1):= Qi od. p:= p–1 front = x:= Q0
Limited Queue
leave from here and shift left
join here
Q
0
pn
43/51

new implementer’s variables: R: [n*X] and f, b: 0,..n
Limited Queue
leave from here and shift left
join here
Q
0
pn
leave from here
leave from here
join here
join here
RR
0fbn 0bfn
data transformer D :
0 ≤ p = b–f < n ∧ Q[0;..p] = R[f;..b] ∨ 0 < p = n–f+b ≤ n ∧ Q[0;..p] = R[(f;..n); (0;..b)] 44/51 ∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ mkemptyq = ∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ (p:= 0) = ∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ pʹ=0 ∧ Qʹ=Q ∧ cʹ=c ∧ xʹ=x = f ʹ=bʹ ∧ cʹ=c ∧ xʹ=x ⇐ f:= 0. b:= 0 Limited Queue 45/51 = fbʹ ∧ b–f=n+bʹ–fʹ
R[f;..b] = Rʹ[(f ʹ;..n); (0;..bʹ)] ∧ xʹ=x ∧ ¬cʹ
f>b ∧ fʹb ∧ fʹ>bʹ ∧ b–f=bʹ–fʹ
R[(f;..n); (0;..b)]=Rʹ[(f ʹ;..n); (0;..bʹ)] ∧ xʹ=x ∧ ¬cʹ
∧ ∨
∧ ∨
∧ ∨
∧
Limited Queue
∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ isemptyq
= ∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ (c:= p=0)
= ∀Q, p· D ⇒ ∃Qʹ, pʹ· Dʹ ∧ cʹ=(p=0) ∧ pʹ=p ∧ Qʹ=Q ∧ xʹ=x
f=b is missing! unimplementable!
46/51