Alagić S., Arbib M.A. — The Design of Well-Structured and Correct Programs :: Электронная библиотека попечительского совета мехмата МГУ

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

Авторизация

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

Alagić S., Arbib M.A. — The Design of Well-Structured and Correct Programs

Alagi&#263 S., Arbib M.A. — The Design of Well-Structured and Correct Programs

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

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

Название: The Design of Well-Structured and Correct Programs

Авторы: Alagić S., Arbib M.A.

Аннотация:

This text synthesizes ten years of research in top-down program design and verification of program correctness. It shows how these techniques may be used in day-to-day programming with the PASCAL language. Many examples of programs and proof development, as well as an explanation of control and data structures, are pro- vided. As a PASCAL programming text, it not only provides a self-contained introduction to the language, but also offers algorithms which operate on sophisticated data structures, and provides the full axiomatic definition of PASCAL in terms of proof rules. Although an introductory course in programmming is required, no particular mathematical background is nec- essary beyond the basic idea of a mathematical proof. A carefully chosen sample of algorithms, including some examples from business data processing, is presented. This collection is supplemented by an extensive set of exercises.

Язык:

Рубрика: Computer science/

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

ed2k: ed2k stats

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

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

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

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

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

abs      68—69
Absolute value      30
Abstract algorithm      10 115
abstract data      115
Abstract expression      152—153
Abstract statement      115 152
action      5
Activation of a procedure      155 189
actual parameter      158—161 253 263
Adaptability of a program      116 138—139 150—151
Adding operators      25 264
Addition of numbers in positional notation      92
Addition of polynomials      209—210
Aho, A.V.      149 216
Alagic, S.      246
Algol      60 26—27 156—158 162 181 10
Algorithm      1 253
Alphabet      11 63 253
Alphabetic change of variables      23—24
AND      262
Antisymmetry      63 253
APPEND      213
Appending a list      213
Approximation      71
Arbib, M.A.      111 246
arctan      69
Array      75—76 78—79 253
Array searching      80—81 237
Array with dynamic bounds      162
Array, parameter      161—163
Array, sorting by merging      127—134
Array, sorting by partitioning      199—201
Array, sorting by selection      123—127
Array, type      267
Array, variable      268
Ashcroft, E.A.      181
assertion      27—28
Assignment rule      38 278
assignment statement      28 253 265
Associated scalar type      67
Associative law      21
Asymmetric algorithm      198
atom      211 253
Back-up      116 133—134
Backtracking      193—197 253
Backus — Naur form      262
Backus, J.      262
Balanced merging      138—139
Base (floating point)      69 253
base type      78 106 269
Basic compositions of actions and their proof rules      29—37
Basic proof rules      38—39
Binary alphabet      13
Binary deletion      217—218
Binary greatest common divisor (algorithm)      223—226
Binary greatest common divisor algortihm      223—226
Binary insertion      217—218
Binary search (of an array)      80—81 237
Binary search of an array      80—81 237
Binary searching      217—218
Binary tree      217
Binomial coefficients      56
Bit      13
BLANK      63
Block      153—158 178—180 253 270 277
Boolean      20—22 65
Boolean expression      20—22 27 254
Boolean operators      20—22 254
Bound occurrence of a variable      24
Bound variable      22—24
Buffer (variable)      76—77 88—89
Business data processing      99—102
Call by name      181
call by reference      160—161 254
Call by value      160—161 254
CAR      211
Cardinality      107 148 254
Cartesian product      60 62—63 76 84 254
case, label      266
case, label list      266
case, list element      266
case, rule      38 278
case, statement      32—33 254 266
CDR      211
char      67
Character set      67—68
chr      67
Circular list      209 254
Cleaning up unstructured algorithms      223—226 243—246 248
Clint, M.      180 181 246
Coarsest partition of a set      145—148
Coarsest partitioning of a set      145—148
Codomain      62 254
Codomain, type      163
Coherent      68
comment      11 17 254
Commutative law      21
Compiler      14 254
Compiling a program      14
Component of a record variable      84—85
Component of an array      75—76 79
Component of an array variable      75—76 79
Component type      78 267
Component variable      267
Composite operation      25
Composition method      254
Composition of statements      29—37
Compound rule      38 278
compound statement      29 254 265
Computation state      15—17 254
Concatenation      76
Conditional rule      38 278
Conditional statement      30—33 254 266
Conjunction      20—21
Cons      212
Consequence rules      27—28 38 278
Constant      254 272 263
Constant definition      72 254 267
Constant definition part      267
Constant identifier      66 72 263
Continuum      71
control variable      268
Conway, R.      52 111 149 246
Copy      213
Copying a list      213 215
Correct refinement      117
correctness      17 19 47 254
Correspondence between formal and actual parameters      158—161 169—170
cos      69
Creating a list      204
Current type of a variable      87
Current value of a variable      72—73
Dahl, O.J.      149
Data type of a variable      57—58 255
De Morgan's laws      21
Debugging      2
declaration      255
Declaration, part      154 178—180 255
Decomposition of a diagram      18
Deletion from a list      207—208
Denotation of integers      70
Denotation of reals      70
Design and correctness of a recursive procedure      199
Design of a recursive procedure      192—198
Design, criteria      116
Desjardins, P.      169
Developing programs with proofs of correctness      2—4 7 19 116—127 139—145 173—178 231—235
Development of a program      115—117 127—139 145—148 193—198
Diagrams with one entry and one exit point      17—18
Difference of sets      60—61 106 258

digit      13 261
Dijkstra, E.W.      149 215 246
Directed graph      202
Disjoint union      61 87 210 255
Disjunction      20—21
Distinctness condition for parameters      172 182
Distribution of runs      129—131 135
Distributive law      21
div      68
Division algorithm      16 39—41 43—45 49
Division of numbers in positional notation      93—95
Domain      62 255
Domain, type      163
doubly linked list      220
dynamic array      162
Dynamic structure      15 255
Dynamic variable      201—202 255
EDGE      202—203 255
Eight queens algorithm      193—198
Eight queens problem      150 193—198
Elements      58—59
Empty set      59
empty statement      28 265
Empty word      63
End of a run      137—138
Endorder      217
Environment      153—154
eof(end of file)      88 102
eoln      103
eq      211
equal      212
Equivalence, class      64 107—110
Equivalence, relation      64 107—108 255
Erathostenes      139
Estimation      71
Euclid      10
Existence of a variable      155
Existential quantifier      22 255
exit      227 231 236 237—238 239—241 244—245
EXP      69
EXPONENT      69 255
Exponential function exp      111
Exponentiation algorithm      54 55
Expression      24—27 265 274
external files      178—179
Factor      24 273 264
Factorial      186 191 219
Failure exit      237—239 247 255
FALSE      20
Fermat      248
Fermat's algorithm      248
fibonacci      183
Fibonacci numbers      183
Field      76 84—85 255
Field, designator      269
Field, identifier      76 84—85 255 269
Field, list      268 275
FILE      76—78 88—89 255
File merging      96—97
File, buffer      269
File, sorting by balanced merging      138—139
File, sorting by natural merging      135—139
File, type      269
File, variable      269
final value      268
find      230—237
first      88
Floating point representation      69 255
Floyd, R.W.      52
Foley, M.      181 216
for, list      268
for, rule      82—83 279
for, statement      81—82 268
Formal parameter      158—161 164 255
Formal parameter section (part)      158 164 271
Free occurrence of a variable      23—24
Free variable      22—24
Function      61—62 163—165 255
Function as a parameter      169
Function, call      164
Function, declaration      163—164 271
Function, designator      263
Function, heading      164 271
Function, identifier      164 263
Function, space      62 255
Generalized greatest common divisor      55
Generalized greatest common divisor algorithm      55
get      77 88 89
Global object      154—156 256
Global variable      153—155
GOTO statement      221—222 256 270
Graph      202 256
Greatest common divisor      2—4 7 45—47 49 187 223—226 256
Gries, D.      52 111 149 181 246
Hoare, C.A.R.      52 110 111 149 180 181 216 246
Hopcroft, J.E.      149
Identifier      12 256 262 272
If statement      266
Implication      21—22
IN      25
Index (of an array)      75—76 79 256
Index, type      78 267
Indexed variable      268
Induction      191 256
Inexact computation      71
infinite loop      36 49—52
Inherent error      71
Initial value      268
Input data      57
Input file      102
Insertion into a list      205—207
Instruction      13 256
INTEGER      68—69
integer arithmetic      68
Intermediate data      57
intersect      214
Intersection of sets      214
Invariant      35 256
Iterative composition      256
Jensen, K.      52 110 111 215
Knuth, D.E.      111 149 216 246
L-statement      227 256
Label      221 256 270
Label, declaration (part)      221 270
Lecarme, O.      169
letter      262
Level of abstraction      115 —117 152—153
Line      103
Linear order      64—66 256
LIST      202—203 256
List copying      213 215
List creation      204
List deletion      207—208
List insertion      205—207
List searching      208
List, copying      213 215
List, creation      204
List, deletion      207—208
List, insertion      205—207
List, searching      208
ln      69
Local object      154—156 256
Local variable      154—156 189
Logarithmic search      80—81
Logical formula      22—24 256
Logical operator      20—22 256
lookup      237—239
Loop      33—37 256
Loop with exits in the middle      239—241 244—245
Loop, invariant      35—36 42 256

1 2 3

О проекте