-
Notifications
You must be signed in to change notification settings - Fork 0
/
Parallel_inc.thy
84 lines (64 loc) · 2.99 KB
/
Parallel_inc.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
(* *********************************************************************
Theory Parallel_inc.thy is part of a framework for modelling,
verification and transformation of concurrent imperative
programs. Copyright (c) 2021 M. Bortin
The framework is distributed in the hope that it will be useful,
but WITHOUT ANY WARRANTY; without even the implied warranty of
MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.
For more details see the license agreement (LICENSE) you should have
received along with the framework.
******************************************************************* *)
theory Parallel_inc
imports RG_tactics
begin
section \<open>Increment a variable in parallel\<close>
record state =
x :: int
a0 :: int
a1 :: int
definition "inc_aux =
INTERLEAVING-BEGIN
\<lbrakk> rely: \<lbrace>\<ordmasculine>a0 = \<ordfeminine>a0 \<and> (\<ordmasculine>x = \<ordmasculine>a0 + \<ordmasculine>a1 \<longrightarrow> \<ordfeminine>x = \<ordfeminine>a0 + \<ordfeminine>a1)\<rbrace>,
pre: \<lbrace> \<acute>x = \<acute>a0 + \<acute>a1 \<and> \<acute>a0=0 \<rbrace>,
post: \<lbrace>\<acute>x = \<acute>a0 + \<acute>a1 \<and> \<acute>a0=1 \<rbrace>
\<rbrakk>
\<langle> \<acute>x:=\<acute>x+1; \<acute>a0:=\<acute>a0 + 1 \<rangle>
\<parallel>
\<lbrakk> rely: \<lbrace>\<ordmasculine>a1 = \<ordfeminine>a1 \<and> (\<ordmasculine>x = \<ordmasculine>a0 + \<ordmasculine>a1 \<longrightarrow> \<ordfeminine>x = \<ordfeminine>a0 + \<ordfeminine>a1)\<rbrace>,
pre: \<lbrace> \<acute>x = \<acute>a0 + \<acute>a1 \<and> \<acute>a1=0 \<rbrace>,
post: \<lbrace>\<acute>x = \<acute>a0 + \<acute>a1 \<and> \<acute>a1=1 \<rbrace>
\<rbrakk>
\<langle> \<acute>x:=\<acute>x+1; \<acute>a1:=\<acute>a1+1 \<rangle>
INTERLEAVING-END"
definition "inc =
INTERLEAVING-BEGIN
\<acute>x:=\<acute>x+1 \<parallel> \<acute>x:=\<acute>x+1
INTERLEAVING-END"
lemma inc_aux:
"\<Turnstile> inc_aux
RELY \<lbrace>\<ordmasculine>x=\<ordfeminine>x \<and> \<ordmasculine>a0=\<ordfeminine>a0 \<and> \<ordmasculine>a1=\<ordfeminine>a1\<rbrace>
PRE \<lbrace>\<acute>x=0 \<and> \<acute>a0=0 \<and> \<acute>a1=0 \<rbrace>
POST \<lbrace>\<acute>x=2 \<and> \<acute>a0=1 \<and> \<acute>a1=1 \<rbrace>
GUAR \<lbrace>True\<rbrace>"
by(unfold inc_aux_def, rg_tac)
definition "r = {(u :: 'a state_scheme, v :: 'a state_scheme) | u v. x u = x v}"
lemma inc_corr :
"\<Turnstile> inc_aux \<sqsupseteq>\<^bsub>r\<^esub> inc"
apply(simp add: inc_aux_def inc_def r_def)
by plain_prog_corr_tac
lemma inc :
"\<Turnstile> inc
RELY \<lbrace>\<ordmasculine>x=\<ordfeminine>x\<rbrace>
PRE \<lbrace>\<acute>x=0\<rbrace>
POST \<lbrace>\<acute>x=2\<rbrace>
GUAR UNIV"
apply(rule prog_corr_RG, rule inc_corr, rule inc_aux)
apply clarsimp
apply(rename_tac s t t')
apply(rule_tac b=s in relcompI, simp)
apply(clarsimp simp: r_def)
apply clarify
apply(rename_tac u)
apply(rule_tac a="u\<lparr> a0 := 0, a1 := 0 \<rparr>" in ImageI)
by(clarsimp simp: r_def)+
end