Müller-Olm M. — Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction :: Электронная библиотека попечительского совета мехмата МГУ

Главная Ex Libris Книги Журналы Статьи Серии Каталог Wanted Загрузка ХудЛит Справка Поиск по индексам Поиск Форум

Авторизация

Поиск по указателям

Müller-Olm M. — Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction

Обсудите книгу на научном форуме

Нашли опечатку?
Выделите ее мышкой и нажмите Ctrl+Enter

Название: Modular Compiler Verification: A Refinement-Algebraic Approach Advocating Stepwise Abstraction

Автор: Müller-Olm M.

Аннотация:

This book presents the verified design of a code generator translating a prototypic real-time programming language to an actual microprocessor, the Inmos Transputer. Unlike most other work on compiler verification, and with particular emphasis on modularity, it systematically covers correctness of translation down to actual machine code, a necessity in the area of safety-critical systems. The formal framework provided as well as the novel proof-engineering ideas incorporated in the verified code generator are also of relevance for software design in general.

Язык:

Рубрика: Computer science/

Статус предметного указателя: Готов указатель с номерами страниц

ed2k: ed2k stats

Издание: 1 edition

Год издания: 1997

Количество страниц: 256

Добавлена в каталог: 25.02.2011

Операции: Положить на полку | Скопировать ссылку для форума | Скопировать ID

Предметный указатель

$E_{0}$       121 122
$E_{1}$       139
$E_{2}$       152 155
$E_{3}$       158
$E_{4}$       163
$F^{\sharp}$       17
$G^{\flat}$       17
$In_{0},..., In_{3}$       118
$I_{1}$       139
$I_{2}$       152
$I_{3}$       158
$I_{4}$       163
$I_{5}$       175
$l_{P}$       138
$l_{W}$       157
$R_{Bool}, R_{Word}$       161
$s_{P}$       138
$s_{W}$       157
$Val_{x}$ , $Val_{c}$       27 95
$\alpha_{0},...,\alpha_{5}$       136
$\Delta$ d      99
$\exists_{x}$ , $E_{x}$       35
$\forall_{x}$ , $A_{x}$       35
$\iota_{u}$       34 35
$\Lambda$ (a, b)      138
$\underline{Prog}$       129
$\underline{Stat}$       129
( $\phi, \pi$ )-path      91
A, B, C      116
Abstraction      3 5 — 40 108 111 135
Abstraction, piecewise      18 107 108
Abstraction, prize of      157
Abstraction, soundness and completeness      155
Addition command      40 57
Addition command, and basic commands      62
Addition command, commutation laws      60
Addition command, dualization and distribution      59
AddOvFl      115
addr      117
Address, admissible      143 144
Addressing mode      116 125
Adjoint, existence and uniqueness      17
Adjoint, lower/upper      15
AdmAdr      143
Alphabet      27
Alphabet, extension/restriction      34
Antitonic      12
Array notation      41 80
Assembler language      5 136
assertion      40 48
Assertion, basic laws      49 50
Assertion, derived laws      55
Assertion, dualization and distribution      48
ASSIGNMENT      40 46
Assignment, basic laws      47 50
Assignment, derived laws      53 55
Assignment, dualization and distribution      46
Assumption      see Assertion
AUX      130
Baddr      117
Base model      3 5 113 135 137 231
BaseAdr      115
Block      40 57
Block code generation      172 — 175 199 219
bool      11
bop      130
Bound, (greatest) lower and (least) upper      9
bpw      114
BYTE      114 118
Byte address      115 116
Byte address, valid      117
Byte selector      115
byteselectlengih, byteselectmask      114
CB      187
CE      186 190
CE’      218
Chain      9
Chan      95
Chaos      40
Choice assignment      40 70
Choice, angelic and demonic      42 51
cm      186
Code      119
Code generator specification, explicit and implicit      179
Code sequence, partitioned      138
Com      42
ComEvt      95
Command      39 42
Command space, heterogeneous      39 40 57 234
Command space, homogeneous      58 — 59 234
Command, basic heterogeneous      57 — 67
Command, basic homogeneous      45 — 56
Command, derived      69 — 81
Command, distribution properties      67 — 69
Command, homogeneous      41 70
Communication event      95
Communication, modeling of      5 41 85 89
Compiler structure      2
Compiler verification      1 — 3 23 179 234
Compiling function      215 220ff
Compiling-correctness      3 128 179ff
Complement      10
Concretization      see Abstraction
Conditional      40 52 78 191
Conditional, generalized      51
Conjunctive, positively      13
Conjunctive, universally      13 17
continuous      13
Control point, symbolic representation of      137ff
Coupling invariant      106
cp      181
CP’      218
CS      185
CS’      218
CurFct      121
CurOpr      122
Data abstraction      108 111
Data refinement      5 39 57 105
Data refinement, functional      106
Data refinement, soundness      106 — 107 110
Deadlock      87 — 90 92 98
Delay      85 99
Deletion command      see Addition command
DICTIONARY      161
Dictionary restriction      see Dictionary extension
Dictionary, (p,ff)-dictionary      218
Dictionary, extension      169ff 177 192 206
Dictionary, standard      161
Dictionary, syntactic      216
Diet, Dictlnfo      161
Direct function      118
Disjointness of program stor¬age and workspace      157 158 183 231
Disjunctive      see Conjunctive
Divergence      87 — 90 92
DivOvFl      115
Duality      43 — 44 46 48 59 71
EB, EE, El, EM, EP, ES      220ff
Eflg      116
Elk      85 95
Embedding      34 82
Estimate, lower/upper      42
Execution cycle      113 120
expr      129 131
Extension, pointwise      12
Failure      103
Failure behavior, acceptable      6 127
FALSE      28 35
FETCH      121 141
fixpoint      14 40
Fixpoint induction principle      227

Formal approach      24
Galois connection      15 44 107 109 111 152 158 159 163
Galois connection, alternative characterization of      16
Galois connection, comparison of      17
Galois connection, composition of      20 — 22
Galois connection, distributive      18 110
General instruction theorem      140 152 158 163
General operation theorem      155 158 163
Hashing      217
Healthiness condition      39
Homogeneous state space      41
HST      85 87 95
IC      173
IC’      218
id      11
Immediate execution idealization      5 129 184
implementation      3 215
Implication order      11 35 41
InCh      130
InChan      95
indelay      123
Independence      26 32
INDEX      117
initialization code      173 — 175 200 220 224
Input process      85 89 96
InStr      118
instr(n)      140
instr(w)      150
InstrCode      119
InstrName      118
Instruction      118
Instruction pointer      116 121 122 125 137
Instruction, current      121
Instruction, effect of      3 — 4 121
Instruction, loading      140
Interface, user and compiler designer      179 230
Interface, verification and implementation      230
InWsp      162
IP      116 138
IpAfter      138
IS      118
JDI      14
Join      9 10
Jump theorem      146 151 153 159 163 176 190 191
Knaster — Tarski theorem      14
Lattice      9 39
Lattice, Boolean      10
Lattice, bounded      10
Lattice, complete      10
Lattice, distributive      10
Lattice, function-      11 — 14
Lattice, sub-      11
Law      4 5 26 39 41 53 85
Law, !-?-sim      71
Law, — -general      61
Law, — $\bigoplus$ -comm      61
Law, -assert      63
Law, --sim      59
Law, $\bigoplus$ — -general      61
Law, $\bigoplus$ — -sim      59
Law, $\bigoplus$ -assume      63
Law, $\Delta$ — -comm      61
Law, $\Delta$ — -general      61
Law, $\Delta$ -add      99
Law, $\Delta$ -assert      99
Law, $\Delta$ -assign      99
Law, $\Delta$ -assume      99
Law, $\Delta$ -bound      103
Law, $\Delta$ -choice      99
Law, $\Delta$ -cond      100
Law, $\Delta$ -refine      99
Law, $\Delta$ -stop      100
Law, $\Delta$ -void      99
Law, $\diamondsuit$ -empty      60
Law, $\diamondsuit$ -reorder      60
Law, $\diamondsuit$ -union      60
Law, ;-cond-leftwards      79
Law, Assert      49
Law, Assert- $\exists$       55
Law, Assert- $\forall$       55
Law, Assert-assume      50
Law, Assert-assume-sim      56
Law, Assert-conj      49
Law, Assert-disj      49
Law, Assert-monotonic      49
Law, Assign-assert      50
Law, Assign-assert1      55
Law, Assign-assert2      55
Law, Assign-assert3      56
Law, Assign-assume      50
Law, Assign-assume1      55
Law, Assign-assume2      55
Law, Assign-assume3      56
Law, Assign-by-choice      77
Law, Assign-cond      79
Law, Assign-output      96
Law, Assume      49
Law, Assume- $\exists$       55
Law, Assume- $\forall$       55
Law, Assume-antitonic      49
Law, Assume-assert      50
Law, Assume-conj      49
Law, Assume-disj      49
Law, Bound-add      102
Law, Bound-asg      103
Law, Bound-comb      102
Law, Bound-cond      103
Law, Bound-final      103
Law, Bound-fixpoint      103
Law, Bound-Id      103
Law, Bound-initial      102
Law, Bound-intro      102
Law, Bound-refine      102
Law, Cancel-asg      53
Law, Cancel1      75
Law, Cancel2      75
Law, Cancel3      75
Law, Cancel4      75
Law, Ch-asg      73
Law, Ch-ass-output      96
Law, Ch-assert1      73
Law, Ch-assert2      77
Law, Ch-assume2      77
Law, Ch-assumel      73
Law, Ch-comm      76
Law, Ch-finalization      74
Law, Ch-Id      72
Law, Ch-initialization-=      74
Law, Ch-mitialization- $\neq$       74
Law, Ch-reorder      72
Law, Ch-union      72
Law, Choice      70
Law, Comb-asg      53
Law, Comb-asgl      47
Law, Comb-assert      49
Law, Comb-assume      49
Law, Comm-asg      53
Law, Conv1      76
Law, Conv2      76
Law, Empty-asg      53
Law, Empty-asg1      47
Law, Exploit-assert      50
Law, Exploit-assume      50
Law, Exploit-cond      79
Law, Final- $\Delta$       99
Law, Final-assert      62
Law, Final-assign      63
Law, Final-assume      62
Law, Final-ch      73
Law, Finalization      63

1 2

О проекте