Goldblatt R. — Axiomatising the Logic of Computer Programming :: Электронная библиотека попечительского совета мехмата МГУ

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

Авторизация

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

Goldblatt R. — Axiomatising the Logic of Computer Programming

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

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

Название: Axiomatising the Logic of Computer Programming

Автор: Goldblatt R.

Аннотация:

This is a small seep for Computer Science: a step towards a systematic proof-theory for programming-language semantics. We study a language that is designed to formalise assertions about how programs behave. In this language each program determines a modal connective that has the meaning "after the program terminates ..,". Such connectives appear in the "algorithmic logic" of A. Salwicki at Warsaw, but the explicit use of techniques from modal logic in this area was initiated more recently by V.R. Pratt at M.I.Т., and has become known as "dynamic logic". It is to the latter that the present work is directly related.

Язык:

Рубрика: Computer science/

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

ed2k: ed2k stats

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

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

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

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

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

-model      260
$\alpha$ -Deduction, Lemma      70
$\alpha$ -Lemma, First      82 96 160 275
$\alpha$ -Lemma, Second      84 96 161 275
$\Lambda$ -consistent      67
$\Lambda$ -consistent in L      140
$\Lambda$ -deducible      66
$\Lambda$ -deducible in L      139
$\Lambda$ -model      71
$\lambda$ -theory      65
$\Lambda$ -theory in L      139
$\Lambda$ -theory, maximal      71
actual parameter      209 213
Admissible form      55 138
Algebra      108 110
Algebraic expression      113
Algorithmic property      184
Alternative command      95
Arithmetical completeness      194
Arithmetical universe      194
Array      251
Assignment command      114
Assignment, rule of      6 26
Axiom Schema      58
Axioms      57 58 87 88 95 137 220 265 285
Base      115
base type      251
Block      208 240
body      207 240
Boolean expression      36
Boolean value      39
Boolean variable      36
Call-by-name      233
Call-by-reference      277ff
Call-by-value      209
Canonical model      76 154 220 242 268
Carrier      110
Characteristic function      41
Command      37
Completeness theorem      77 162
Component type      251 257
composition      16 47
Composition, rule of      11
Conditional connective      37
Conditional rule      16
Consequence (rule of)      7 14
Consistent strongly      165
Consistent, $\Lambda$       67
Consistent, $\Lambda$ in L      139
Constant      108 110
Constant, equation      173
Constant, expression      111
Correct interpretation      6
correctness      3ff
Correctness, partial      15
Correctness, total      15
Data type      108ff 176ff
Deducible      58ff
Deducible strictly      165
Deducible, $\Lambda$       66
Deducible, $\Lambda$ in L      139
Deduction Lemma, $\alpha$       70
Deduction Theorem      68
Deductively closed      67
Detachment      58
Determinism      29 87ff
Diagram      152 173
Dummy Rule      22
Dynamic logic      193
e-model      217
E-model, standard      218
E-sequence      236
Empty command      22
Environment      214 241
Equality relation      41
Equational theory      173
Equivalence of programs      28
Expression      36
Expression, algebraic      113
Expressive      190
External logic      2
First $\alpha$ -Lemma      82 96 160 275
First-order formula      114
First-order logic      5
Fixed point      53
Formal parameter      207
Formula      38
Formula, first-order      114
Free occurrence      26 178ff
function call      209
Function declaration      207
function designator      209 213
Functional relation      43
Fundamental theorem      77
Fundamental Theorem for $M^C_{\Delta}$       276
Fundamental Theorem for $M_{\Delta}$       161
Global variable      208
Guarded command      96
Has enough states      120 263
Hoare's Iteration Rule      9 63

Holds      31 42
Implication connective      38
Incomplete system      19
Index (type)      251 254 257
Indexed variable      252 258
Infinitary rule      22
Internal logic      2 40
Interpretation      6
Invariant      9
Isomorphic      167
Iteration rule      9 58
Language      113
Local variable      208 238
Logical system (logic)      57 59 139 266
Main variable      214
Maximal $\Lambda$ -theory      71
Maximal $\Lambda$ -theory in L      140
Meta-variable      58
Metalanguage      3
Minimal subalgebra      112
Modal logic      17
Model      39 43 115 164
Model, $\Lambda$       71
Model, canonical      76 154 220 242 268
Model, E      217
Model, natural      122 220 242
Model, standard      47 48 121 218 260 273
Natural model      122 220 242
Non-determinism      95ff
Non-recursive      236
Omega Rule      23 175
Omega-Iteration Rule      58
powerset      109 304
Procedure declaration      238
Procedure identifier      240
Process logic      200
Program letter      37
Propositional calculus      59
RECURSIVE      235
Relettering      139
Rich theory      144 266
Rigid designator      116
Rule, A      175
Rule, assignment      6 26
Rule, composition      11
Rule, consequence      7
Rule, detachment      58
Rule, infinitary      22
Rule, invocation      243
Rule, iteration      9 58
Rule, omega      23 175
Rule, omega-iteration      58
Rule, substitution      243
Rule, terminal implication      60
Rule, termination      58
Rule, universal generalisation      138
Satisfaction      42
Satisfaction, simultaneous      79
scalar      254 256 257
Second $\alpha$ -Lemma      84 96 161 275
Sentence      118
Sequent      184
Sequential connectives      40
Side effect      210 225
Signature      109
SIMPLE      214 219 241
sort      109
Standard model      47 48 95 121 218 260 273 289
State      30 39
Step-wise refinement      17
Strictly deducible      165
String      109
Strong completeness      78 163
Strongest post-condition      190
Strongly consistent      165
Subalgebra      21
Tautology      60
Temporal logic      197
Terminal implication rule      58
Termination      13 25
Termination rule      58
test command      93
Theory, $\Lambda$       65
Theory, $\Lambda$ in L      139
Theory, maximal      71
Theory, maximal in L      140
Theory, rich      144 266
Top-down design      17
TYPE      214
Undefined expression      30
Universal generalisation      138
Valid      43
Valuation      39 115 259
Valuation, total      118
Value parameter      233 240
Value substitution      209
Variable declaration      208
Variable parameter      233 240
Weakest liberal pre-condition      91
Weakest pre-condition      90 191
witnesses      144

О проекте