proof system

Assignment axiom

pre→post[eˉ/xˉ](pre∧⌈xˉ′=eˉ⌉)→guarprestablewhen‾relypoststablewhen‾relyxˉ:=eˉsat‾(pre,rely,guar,post)‾pre \to post[ \bar e/ \bar x] \\ (pre \land \lceil \bar x'= \bar e \rceil ) \to guar \\ pre \ \underline {stable \ when} \ rely \\ { post \ \underline {stable \ when} \ rely }\\ \overline{ \bar x:= \bar e \ \underline{sat} \ (pre, rely ,guar ,post)}pre→post[eˉ/xˉ](pre∧⌈xˉ′=eˉ⌉)→guarpre stable when relypost stable when relyxˉ:=eˉ sat (pre,rely,guar,post)
where⌈xˉ=eˉ⌉=def(xˉ′=eˉ∨x′=x)∧∀z∈(y−xˉ).z′=zwhere \lceil \bar x = \bar e \rceil \ \overset {def}{=} (\bar x' = \bar e \lor x'=x)\land \forall z \in (y- \bar x). z' =z where⌈xˉ=eˉ⌉ =def(xˉ′=eˉ∨x′=x)∧∀z∈(y−xˉ).z′=z

An example :x:=10sat‾(true,x>0→xˉ≥x,true,x≥10)x:=10 \ \underline {sat} \ (true ,x>0 \to \bar x \ge x ,true ,x \ge 10) x:=10 sat (true,x>0→xˉ≥x,true,x≥10)
证：1、pre→post[eˉ/xˉ]⊨true→x≥10[10/xˉ]=true成立2、pre∧⌈xˉ′=eˉ⌉)→guar⊨true∧x′=10→true成立3、prestablewhen‾rely⊨true∧x>0→true成立4、poststablewhen‾rely⊨x≥10∧x>0→x′≥x⇒x′≥10成立x:=10sat‾(true,x>0→xˉ≥x,true,x≥10)1、pre \to post[ \bar e/ \bar x] \vDash true \to x\ge 10[10/ \bar x] =true\ 成立 \\ 2、pre \land \lceil \bar x'= \bar e \rceil ) \to guar \vDash true \land x'=10 \to true 成立 \\ 3、 pre\ \underline {stable \ when} \ rely \vDash true \land x \gt 0 \to true\ 成立 \\ 4、 post \ \underline {stable \ when} \ rely \vDash x \ge 10 \land x \gt 0 \to x' \ge x \Rightarrow x' \ge 10 成立 \\ x:=10 \ \underline {sat} \ (true ,x>0 \to \bar x \ge x ,true ,x \ge 10) \\ 1、pre→post[eˉ/xˉ]⊨true→x≥10[10/xˉ]=true 成立2、pre∧⌈xˉ′=eˉ⌉)→guar⊨true∧x′=10→true成立3、pre stable when rely⊨true∧x>0→true 成立4、post stable when rely⊨x≥10∧x>0→x′≥x⇒x′≥10成立x:=10 sat (true,x>0→xˉ≥x,true,x≥10)

Await axiom

prestablewhen‾relypoststablewhen‾relyPsat‾(pre∧b∧y=v0,y′=y,true,guar[v0/y,y/y′]∧post)‾awaitbthenPendsat‾(pre,rely,guar,post)pre\ \underline {stable\ when} \ rely \\ post\ \underline {stable\ when }\ rely \\ \underline{ P\ \underline {sat}\ (pre \land b \land y=v_0,y' =y,true,guar [ {v_0/y,y/y'}] \land post)} \\ { await\ b\ then\ P\ end\ \underline {sat} (pre,rely,guar ,post) } pre stable when relypost stable when relyP sat (pre∧b∧y=v0,y′=y,true,guar[v0/y,y/y′]∧post)await b then P end sat(pre,rely,guar,post)

An example : awaitx>0thenx:=x−1endawait \ x\gt 0\ then\ x:=x-1\ \ end await x>0 then x:=x−1 end
satisfies (x≥0,x≥0→x′≥0,x′≤x,x≥0)(x \ge 0,x \ge0 \to x' \ge 0,x' \le x,x \ge 0)(x≥0,x≥0→x′≥0,x′≤x,x≥0)

Consequence rule

pre→pre1,rely→rely1,guar1→guar,post1→postPsat(pre1,rely1,guar1,post1)‾Psat‾(pre,rely,guar,post)pre \to pre_1,rely \to rely_1, \\guar_1\to guar, post_1 \to post \\ \underline {P{sat}\ (pre_1,rely_1,guar_1,post_1) } \\P\ \underline{sat}\ (pre,rely,guar,post)pre→pre1,rely→rely1,guar1→guar,post1→postPsat (pre1,rely1,guar1,post1)P sat (pre,rely,guar,post)

An example: x:=10sat‾(x=−2,x>0→x′≥x,,true,x≥10∨x=−6)x:=10\ \underline{sat}\ (x=-2,x \gt 0 \to x' \ge x,,true,x \ge10 \lor x=-6)x:=10 sat (x=−2,x>0→x′≥x,,true,x≥10∨x=−6)

Sequential composition rule

Psat‾(pre,rely,guar,mid)Qsat‾(mid,rely,guar,post)P;Qsat‾(pre,rely,guar,post)‾P\ \underline {sat}\ (pre,rely,guar,mid) \\ Q\ \underline{sat}\ (mid,rely,guar,post) \\ \overline{P;Q \underline {sat}\ (pre,rely,guar,post)}P sat (pre,rely,guar,mid)Q sat (mid,rely,guar,post)P;Qsat (pre,rely,guar,post)

An example:
x:=x+1sat‾(x≥x0,x0≤x→x≤x′,x′≥x,x≥x0+1)x:=x+1sat‾(x≥x0+1,x0≤x→x≤x′,x′≥x,x≥x0+2)x:=x+1;x:=x+1sat‾(x≥x0,x0≤x→x≤x′,x′≥x,x≥x0+2)x:=x+1\ \underline {sat}\ (x \ge x_0,x_0 \le x \to x \le x',x' \ge x,x \ge x_0+1) \\ x:=x+1\ \underline{sat}\ (x \ge x_0+1,x_0 \le x \to x \le x' ,x' \ge x,x \ge x_0+2 ) \\ x:=x+1;x:=x+1\ \underline{sat}\ (x \ge x_0,x_0 \le x \to x \le x',x' \ge x,x \ge x_0+2)x:=x+1 sat (x≥x0,x0≤x→x≤x′,x′≥x,x≥x0+1)x:=x+1 sat (x≥x0+1,x0≤x→x≤x′,x′≥x,x≥x0+2)x:=x+1;x:=x+1 sat (x≥x0,x0≤x→x≤x′,x′≥x,x≥x0+2)

Conditional rule

prestablewhen‾relyPisat‾(pre∧bi,rely,guar,post)skipsat‾(pre∧¬(b1∨⋯∨bn),rely,guar,post)ifb1→p1□…□bn→Pnfisat‾(pre,rely,guar,post)‾pre\ \underline{stable\ when }\ rely \\ P_i\ \underline{sat}\ (pre \land b_i,rely,guar,post) \\ skip\ \underline{sat}\ (pre \land \lnot(b_1 \lor \dots \lor b_n),rely ,guar,post) \\ \overline{if\ b_1 \rightarrow p_1 \square \dots \square b_n \to P_n\ fi\ \underline {sat} \ (pre ,rely,guar,post)}pre stable when relyPi sat (pre∧bi,rely,guar,post)skip sat (pre∧¬(b1∨⋯∨bn),rely,guar,post)if b1→p1□…□bn→Pn fi sat (pre,rely,guar,post)

An example: ifx<10→x:=10fisat‾(true,x≤x′,x<x′,x≥10)if\ x \lt10\ \to x:=10\ fi\ \underline{sat}\ (true,x \le x',x \lt x',x \ge10) if x<10 →x:=10 fi sat (true,x≤x′,x<x′,x≥10) `

x:=10sat‾(x<10,x≤x′,x≤x′,x≥10)andskipsat‾(x≥10,x<x′,x<x′,x≥10)x:=10\ \underline{sat}\ (x \lt 10,x \le x',x \le x',x \ge 10) \\ and\ skip\ \underline{sat}\ (x \ge 10 ,x \lt x',x \lt x',x \ge 10)x:=10 sat (x<10,x≤x′,x≤x′,x≥10)and skip sat (x≥10,x<x′,x<x′,x≥10)

Iteration rule

prestablewhen‾relypre∧¬b→postpoststablewhen‾relyPsat‾(pre∧b,rely,guar,pre)whilebdoPodsat‾(pre,rely,guar,post)‾pre\ \underline {stable \ when}\ rely \\ pre \land \lnot b \to post \\ post\ \underline{ stable \ when}\ rely \\ \bm P\ \underline{sat} \ (pre \land b ,rely ,guar,pre) \\ \overline{ \bm {while}\ b\ \bm {do}\ P\ \bm {od}\ \underline{sat}\ (pre,rely,guar,post)}pre stable when relypre∧¬b→postpost stable when relyP sat (pre∧b,rely,guar,pre)while b do P od sat (pre,rely,guar,post)

An example:
whilebdoPodsat‾(true,x≤x′,x≤x′,x>10)\bm {while}\ b\ \bm{do}\ P\ \bm {od}\ \underline{sat}\ (true,x \le x' ,x \le x' ,x \gt 10)while b do P od sat (true,x≤x′,x≤x′,x>10)
## Parallel rule
(rely∨guar1)→rely2(rely∨guar2)→rely1(guar1∨guar2)→guarpsat‾(pre,rely1,guar1,post1)Qsat‾(pre,rely2,guar2,post2)P∣∣Qsat‾(pre,rely,guar,post1∧post2)‾(rely \lor guar_1) \to rely_2 \\ (rely \lor guar_2) \to rely_1 \\ (guar_1 \lor guar_2) \to guar \\ \bm p\ \underline{sat}\ (pre ,rely_1,guar_1,post_1) \\ \bm Q\ \underline{sat}\ (pre ,rely_2,guar_2,post_2) \\ \overline {P || Q \ \underline {sat}\ (pre,rely ,guar ,post_1 \land post_2)} (rely∨guar1)→rely2(rely∨guar2)→rely1(guar1∨guar2)→guarp sat (pre,rely1,guar1,post1)Q sat (pre,rely2,guar2,post2)P∣∣Q sat (pre,rely,guar,post1∧post2)

Auxiliary variable rule

∃z.pre1(y,z,y0)∃z′.rely1((y,z).(y′,z′),y0)Psat‾(pre∧pre1,rely∧rely1,guar,post)‾Qsat‾(pre,rely,guar,post)\exists z. pre_1(y,z,y_0) \\ \exists z'.rely_1((y,z).(y',z'),y_0) \\ \underline{\bm P\ \underline {sat}\ (pre \land pre1,rely \land rely_1,guar,post)}\\ \bm Q \underline{sat}\ (pre,rely,guar,post)∃z.pre1(y,z,y0)∃z′.rely1((y,z).(y′,z′),y0)P sat (pre∧pre1,rely∧rely1,guar,post)Qsat (pre,rely,guar,post)

An example:x:=x+1∣∣x:=x+1x:=x+1 || x:=x+1x:=x+1∣∣x:=x+1

The Rely-Guarantee Method for Verifying Shared Variable Concurrent Program 正确性公理相关推荐

FORM级别和数据库级别的Trace
metalink上的文章较全的,中文的可参考我的博客EBS开发技术之trace http://blog.csdn.net/cai_xingyun/article/details/17250971 ...
LOB variable no longer valid after subsequent fetch
cx_oracle读取oracle wm_concate函数操作过后的长文本clob字段,当使用fetchall或者fetchmany读取数据时,报上面的错参考下面的文档,发现只能使用下面2种方式中 ...
Oracle大数据量读取：LOB variable no longer valid after subsequent fetch
Stack Overflow解决方案: cx_Oracle版本问题,在cx_Oracle5版本上有部分限制,在cx_Oracle6版本上没有此项限制. This is a limitation of ...
【已解决】运行Eclipse出错：Failed to load the JNI shared library
[问题] 运行Android的ADT,即Eclipse出错: Failed to load the JNI shared library C:\Program Files (x86)\Java\jre ...
java中stack heap_java虚拟机中的堆（heap）、栈（stack）、方法区(method area)
1.堆区存储的全部是对象,每个对象都包含一个与之对应的class的信息.(class的目的是得到操作指令) jvm只有一个heap区,被所有线程共享,不存放基本类型和对象引用,只存放对象本身堆的优 ...
vvvvvvvvvvvvvvvvvvvvvvvvv
Java Concurrency In Practice Brian Göetz Tim Peierls Joshua Bloch Joseph Bowbeer David Holmes Doug L ...
Understanding JVM Internals---不得不转载呀
http://www.cubrid.org/blog/dev-platform/understanding-jvm-internals/ http://architects.dzone.com/art ...
Lock-Free 编程
文章索引 Lock-Free 编程是什么? Lock-Free 编程技术读改写原子操作(Atomic Read-Modify-Write Operations) Compare-And-Swap 循 ...
Pthread：POSIX Threads Programming
POSIX Threads Programming Blaise Barney, Lawrence Livermore National Laboratory 译文点此 Table of Conten ...

The Rely-Guarantee Method for Verifying Shared Variable Concurrent Program 正确性公理

文章目录