|
|
 |
| Авторизация |
|
|
|
| Поиск по указателям |
|
|
|
|
|
|
|
 |
|
|
|
| Müller-Olm M. — Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction |
|
|
|
| Предметный указатель |
Law, Finalizationl 63
Law, Identity-asg 47
Law, Initial- 99
Law, Initial-assert 62
Law, Initial-assign 62
Law, Initial-assume 62
Law, Initial-ch- 73
Law, Initial-ch-= 73
Law, Initial-output 96
Law, Initial-stop 98
Law, Initialization 63
Law, Input-asg 96
Law, Proper-ini 63
Law, Reorder-asg 47
Law, Restrict-angel 63
Law, Restrict-demon 63
Law, S-comb 31
Law, S-embedding 34
Law, S-empty 31
Law, S-equality 35
Law, S-exists 37
Law, S-forall 37
Law, S-reorder 31
Law, S-void 31
Law, Span 52
Law, Span1 56
Law, Stop-zero 98
Law, V-cancel 27
Law, V-commute 27
Law, V-void 27
Law, Void-bound 102
Law, Void-cond 79
LDT 148
Lifting 25 28 82
Loaded 138
Loader, obligation of 120 183 216 231
Loading time 148
Loop 86 134
Loop, adequacy of fixpoint definition 91 — 94
Loop, translation of 202 — 204 223 226ff
Machine program 113 118 137
MDI 14
Me 133
Mechanical verification 3 234
Meet 9 10
MEM 117
Memory 116 — 118 125 156 160 180
Miracle 24 40
Modularity 79 122 124 143 180 234
Modularization lemma 78
Monotonic 12
Mop 130
MostNeg, MostPos 114
MP 133
ms 133
MulOvFl 115
Nibble 114
op 119 150
Opcode 119
Operand register 116 125 147ff
Operands, word-size 147ff
Operation 119 122 154
Operational semantics 87 — 95
OprName 119
Oreg 116
OutCh 130
OutChan 95
outdelay 124
Output process see Input process
Overloading 29 34
Parameterization, implicit 139 215
Partial correctness 88
Partial order 9
Partially ordered set 9
Pred 95
Predicate 28 35
Predicate transformer 5 24 39 41
Predicate transformer, dualization 43
Predicate transformer, monotonic 39 42
Prefix 148ff
Prefixing 148
proc 96
Process 96
| ProCoS 2
PROG 131
Program counter see Instruction pointer
Program storage 138 183
Projection 28
PTRANS 41
Quantification 35 — 38 55
Reasoning language 23 — 24
Reasoning, formal and informal 155 235
Referential transparency 25
refinement 15 17 42 89 122
Refinement algebra 4 5 23 39ff 57 70 81 108
Refinement, operational interpretation 89
Refusal set 94
Reg 175
register 116 175
Representation relation 160 185
Representation relation, surjective 170ff 192
Reset 120
Retrieve mapping 105
Reuse 234
Run 120
SE 131
Self-modifying code 2 113 124 138
Shift of excess time 6 129 184 189
Simulation 44
sp 131
SS 131
Standard ML 217 230
STAT 131
State 27
State, proper 87
State, variation of 27
STEP 120
Stop process 85 98
Strict 12
Sub/super-distributive 13
SubOvFl 115
Substitution 26 30 47
Substitution, equality and 35
Substitution, quantifiers and 37
Symbol table 162 179
Symbolic addressing 160ff
SyntDict, SyntDictlnfo 216 217
TC 120
Termination 88
Time 98
Time bound 85 101
Time stamp 95
Timing 5 — 6 41 85 104 123 128 134 184 189 194 198 230 236
Total correctness 86 88
TPL, definition of 127 — 134
Trace 85 87 94 95 103
Transfer lemma 14
Translation theorem 3 179 189ff 215 230 233
Translation theorem, refined 218 — 220
Translation, expressions 186 192 204 220
Translation, programs 181 193 220 222
Translation, statements 184 194ff 220 222
Transputer 2 5 119
TRUE 28 35
Undefined expressions 23 127 187 209 213
VALFCT 95
Validation 1
Valuation function 24 28
Variable 25 26 130 160 175 204
Variable, domain of 27
Variable, meta- 25 82
VDM 86 105
view 3 5 135 177 235 237
Weakest precondition 39 88
Word 114
Word address 115 — 116
Word operators 115
WordAdr 116
Wordlength 114
Workspace 156ff 160 183
Wp-calculus 5 39
Wptr 116 157
WspInMem 158
X 26
Y 95
Z 130
{|u|} 27
|
|
|
| Реклама |
|
|
|
|
|
О проекте