I 开篇
II 离散数学
2. 数 (已看)
III 简单RSL
IV 规约类型
VI 其他
1. 绪论
1.1 准备
工程是将科学的洞察力和人类的需求转换为技术产品的数学,职业,规范,工艺和艺术. 软件工程的科学是计算机与计算的科学
计算机科学是什么样的"事物"可以(或能够)存在于计算机"之中",也就是说,数据(即值及其类型)和进程,及其函数,事件和通信的研究和知识
计算科学是如何构造这些"事物"的研究和知识
1.2 软件工程三部曲
1.2.1 软件和系统开发
通过计算系统, 我们指共同实现某需求的硬件和软件的组合
1.2.2 三部曲引出
在我们能够(3)设计软件之前,我们必须理解(2)对该软件的需求.在我们能够规定(2)需求之前,我们必须理解应用(1)领域
1.2.3 领域工程
通过领域工程,我们指领域描述的工程
通过领域,我们指(i)人类活动的范围,(ii)和/或半机械化或全机械化的行为,(iii)可以被描述的自然范围,潜在地能够得以部分或完全计算的部分或全部
1.2.4 需求工程
1.2.5 软件设计
1.2.6 讨论
1.3 文档
1.3.1 文档种类
1.3.2 时期,阶段和步骤文档
1.3.3 信息文档
1.3.4 描述文档
1.3.5 分析文档
1.4 形式技术和形式工具
1.4.1 关于形式技术和语言
1.4.2 软件工程教材中的形式技术
1.4.3 一些程序设计语言
1.4.4 一些形式规约语言
1.4.5 目前形式语言的不足
1.4.6 其他的形式工具
1.4.7 为什么要形式技术和形式工具
1.5 方法和方法学
1.5.1 方法
方法,通过其我们理解为了有效地构造一个有效的人工制品,这里是软件(即一个计算系统),选择和应用许多分析和合成(构造)技术和工具的一组原则
1.5.2 方法学
方法学,通过其我们理解对一个或者多个方法的研究及其知识
1.5.3 讨论
原则将由人来解释.选择和分析在绝大多数情况下也由人来进行.一些技术和一些工具可以由机器来使用,即形式化.但是这还远不是全部.因此说形式方法的概念是一个不恰当的名字.似乎更适宜说一些技术和一些工具是形式的.因此我们做出结论: 方法不能是形式的
1.5.4 元方法学
1.6 软件基础
1.6.1 教学法和范式
1.6.2 语用,语义和句法
1.6.3 规约和程序设计范式
1.6.4 描述,规定和规约
1.6.5 元语言
1.6.6 总结
1.7 目标和效果
1.7.1 目标
1.7.2 效果
1.7.3 讨论
1.8 文献评注
1.9 练习
2. 数
Kronecher 说过,或者人们认为他这样说过, "上帝创造了整数,所有其他都是人类的作品"
2.1 引言
2.2 数符和数
数符是数的名称.没有人曾经(在头脑清醒的状态下)见过数.数是抽象的数学量.它们的特点是其性质.每一个存在于数学域中的数都有确切的一个拷贝: 原始的数.许多数有简单的名称,并且相同的一个数常常有不止一个不同的简单名称: 7,seven,sieben,sept,syv,...
数字,我们通过其理解某个特定数的简单数符
2.3 数的子集
2.3.1 自然数: Nat
令Nat表示全体自然数的集合,并根据以下BNF(Backus Normal (or Naur) Form)语法书写自然数:
<NatNum> ::= <DecDig> | <DecDig><NatNum>
<DecDig> ::= 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9
<DecDig> 代表十进制数位
例2.1 十进制数字自然数数符的语义.让我们来做下列思考性的实验: 令0,1,2,3,4,5,6,7,8,9从左到右"设法表示"和十进制数字0,1,2,3,4,5,6,7,8,9相应的自然数: 则
M: <NatNum> -> Num
M(d,n) ≡ 10 * M(d) + M(n)
M(d) ≡ case d of 0->0, 1->1, ..., 9->9 end
非形式地说明了自然数数符的含义
例2.2 "四元一组"二进制数字自然数数符的语义.我们用"四元一组"的二进制数符来表示一个或多个特定的由0和1组成的四元一组, 即: 0000, 0001, 0010, 0011, ..., 1000, 1001. 那么我们再次得到相同的右侧描述:
type
<QuaNum> ::= <QuaNum><QuaDig> | <QuaDig>
value
M: <NatNum> -> Num
M(d,n) ≡ 10 * M(d) + M(n)
M(d) ≡ case d of 0000->0, 0001->1, ..., 1000->8, 1001-> 9 end
对一些RSL结构的解释
换句话说, 结构 "case e of p1->e'1, p2->e'2,...pn->e'n end" 的第一个参数是一个可为任意值和类型的表达式. 第二个参数是一个由逗号隔开的"三元组"序列: pi->e'i, 紧跟关键字of 之后的第一个三元组中i为1,其次为2,并依此类推.如果e的值能够表示为模式,像此处包括某个模式的所有值,那么整个case结构的值就是e'i的值，否则我们试着比较下一个三元组.如果没有三元组产生相等的比较, 即"匹配",那么整个表达式(整个case结构)的值为chaos
2.3.2 整数: Int
性质
令a,b和c代表整数.一些整数的重要性质是
[ + 和 * 的结合律和交换律: ]
a + (b + c) = (a + b) + c, a + b = b + a
a * (b * c) = (a * b) * c, a * b = b * a
[ * 对于 + 的分配律: ]
a * (b + c) = a * b + b * c
[ 0 和 1 的性质 ]
0 + a = a, 1 * a = a, 0 * a = 0
[ - 的性质 ]
(-a) + a = 0, (-a) * b = -(a * b), (-a) * (-b) = a * b
[ 消去律 ]
a + b = a + c => b = c, a != 0 -> (a * b = a * c => b = c)
[ 序的性质 ]
a > 0 ^ b > 0 => a * b > 0
∀ a:Int • a < 0 V a = 0 V a > 0 [ 三分法 ]
[ 加法和乘法的定义 ]
s:Int -> Int, s(i) ≡ i + 1 ≡ i'
a + 0 = a, a + s(b) = s(a + b) = a + b + 1
a * 0 = 0, a * s(b) = (a * b) + a
[ 整数除法 ]
a / b as (q, r) 这里 a = b * q + r ^ 0 <= r < b
2.3.3 实数: Real
有限可写实数: dndn-1...d1.d'1d'2...d'm-1d'm
双重无限可写的实数: ...d''id''i-1...d''1.d'''1d'''2...d'''j-1d'''j...
有理数
Rat = { | i/j • i, j : Int ^ j != 0 | }
2.3.4 无理数
无理数是所有其他非有理数的实数
2.3.5 代数数
代数数是所有满足下列形式多项式方程的根r的实数或虚数: a * xn + b * xn-1 + ... + c * x + d = 0
其中n是任一整数,系数a,b,...,c,d是整数.√ 2 是一个代数数.根是使多项式: a * xr + b * xr-1 + ... + c * x + d 的值为0的任何数r
2.3.6 超越数
非代数数的实数被称作超越数. 超越数的例子如 e 和 π
2.3.7 复数和虚数
复数是作为某种多项式方程的解而出现的. 在一般数学中, 这种数(c)通常写作一对实数(a)和虚数(ib)(其中a和b本身是实数): c: a + ib
type
Complex = Real x Real
value
add, sub, mpy, div: Complex x Complex -> Complex
add((a1, ib1), (a2, ib2)) ≡ (a1 + a2, ib1 + ib2)
sub((a1, ib1), (a2, ib2)) ≡ (a1 - a2, ib1 - ib2)
mpy((a1, ib1), (a2, ib2)) ≡ (a1 * a2 - ib1 * ib2, a1 * ib2 + a2 * ib1)
div((a1, ib1), (a2, ib2)) ≡ ...
2.4 类型定义: 数
那么在什么时间和场合,数被用于对论域, 需求和软件建模呢?当对这些现象和概念的操作需要诸如加法,减法,乘法和较少出现的除法操作的时候,我们用数对某些(具体的)现象和某些(抽象的)概念建模
一个(具体的)类型定义把一个类型表达式和一个类型名称联系起来.
在本章介绍的类型表达式是:
type
Nat, Int, Real
令N,I和R表示(任意选取的)类型名称,则类型定义的例子是:
type
N = Nat
I = Int
R = Real
N代表自然数值的类型(即类).I 和 R 代表整数和实数值的类型
我们可以把身高,体重和一个人联系起来.可以把人口(即公民的数量),男女的划分和一个国家联系起来.可以把一个人口和此人口的年度增加量或缩减量(即偏移量),和此人口联系起来.因此建议的类型是:
type
Height, Weight = Real
Population, Female, Male = Nat
Deviation = Int
上述内容仅是我们为各"类"现象和概念建模的初步探讨
2.5 总结
2.6 文献评注
2.7 练习
3. 集合
3.1 背景
3.2 数学的集合
3.3 特殊集合
3.3.1 外延公理
3.3.2 划分
3.3.3 幂集
3.4 分类和类型定义: 集合
3.4.1 集合抽象
3.4.2 集合类型表达式和类型定义
3.4.3 分类
3.5 RSL中的集合
3.6 文献评注
3.7 练习
4. 笛卡尔
4.1 要点
4.2 笛卡尔值表达式
4.3 笛卡尔类型
4.4 笛卡尔的目
4.5 笛卡尔的相等
4.6 一些构造的例子
4.7 分类和类型定义: 笛卡尔
4.7.1 笛卡尔抽象
4.7.2 笛卡尔类型表达式和类型定义
4.8 RSL中的笛卡尔
4.9 文献评注
4.10 练习
5. 类型
5.1 值和类型
5.2 现象和概念类型
5.2.1 现象和概念
5.2.2 实体: 原子和复合
5.2.3 属性和值
5.3 程序设计语言类型概念
5.4 分类或抽象类型
5.5 内建和具体类型
5.6 类型检查
5.6.1 类型确定的变量和表达式
5.6.2 类型错误
5.6.3 类型错误检测
5.7 类型作为集合,类型作为格
5.8 总结
5.9 练习
6. 函数
6.1 概述
6.2 要点
6.2.1 背景
6.2.2 一些函数概念
6.3 函数是如何产生的
6.4 关于求值概念的题外话
6.4.1 求值,解释和细化
6.4.2 两个求值的例子
6.4.3 函数调用
6.5 函数代数
6.5.1 代数
6.5.2 函数类型
6.5.3 高阶函数类型
6.5.4 非确定性函数
6.5.5 常量函数
6.5.6 严格函数
6.5.7 严格函数和严格函数调用
6.5.8 函数上的操作
6.6 Curry化和λ记法
6.6.1 Curry化
6.6.2 λ记法
6.6.3 Curry化和λ记法的例子
6.7 关系和函数
6.7.1 谓词
6.7.2 通过关系搜索的函数求值
6.7.3 非确定性函数
6.8 类型定义
6.9 结论
6.10 文献评注
6.11 练习
7. λ演算
7.1 非形式介绍
7.2 "纯"λ演算句法
7.3 λ演算的运用
7.4 "纯"λ演算语义
7.4.1 *和约束变量
7.4.2 绑定和辖域
7.4.3 变量的冲突和混淆
7.4.4 带入
7.4.5 α转换和β转换规则
7.4.6 λ转换
7.5 名调用和值调用
7.6 Church-Rosser定理----非形式版本
7.7 RSLλ记法
7.7.1 扩展λ表达式
7.7.2 "let...in...end"结构
7.8 不动点
7.8.1 要点
7.8.2 非形式概述
7.8.3 不动点操作符Y
7.8.4 不动点求值
7.9 讨论
7.9.1 概述
7.9.2 关于最小,最大,全部不动点
7.9.3 强调
7.9.4 原则,技术和工具
7.10 文献评注
7.10.1 参考文献
7.10.2 Alonzo Church, 1903-1995
7.11 练习
8. 代数
8.1 引言
8.2 代数概念的形式定义
8.3 代数是如何产生的
8.4 代数的种类
8.4.1 具体代数
8.4.2 抽象代数
8.4.3 异构代数
8.4.4 泛代数
8.5 规约代数
8.5.1 表达代数的句法方式
8.5.2 一个栈代数的例子
8.5.3 一个队列代数的例子
9. 数理逻辑
10. RSL中的原子类型和值
11. RSL中的函数定义
12. 面向性质与面向模型的抽象
13. RSL中的集合
14. RSL中的笛卡尔
15. RSL中的列表
16. RSL中的映射
17. RSL中的高阶函数
18 RSL中的类型
19. 应用式规约程序设计
20. 命令式规约程序设计
21. 并发式规约程序设计
22. 其他
术语表
1. 抽象(Abstract): 关注于本质性质的某事物. 抽象是一个关系: 对于其他(具有----被认为是----非本质性质的)某事物来说,某事物是抽象
2. 抽象代数(Abstract algebra): 抽象代数是用规定函数的一般性质而非函数值的公设(公理,定律)来定义载体元素和函数的代数.(抽象代数也成为公设代数或公理代数. 研究代数的公理方法构成通常被称作现代代数的基石)
3. 抽象数据类型(Abstract data type): 抽象数据类型是值的集合以及在这些数据值上抽象定义的函数的集合, 并且没有定义这些值的外部世界或计算机(即数据)表示
4. 抽象(Abstraction): "抽象的艺术,思考中的分离行为; 纯粹的观念: 想象的某事物"
5. 抽象函数(Abstraction function): 抽象函数是应用于具体类型(concrete type)的值(value)上并产生----被称为相应的----抽象类型(abstract type)的值的函数(与检索函数(retrieve function)一样
6. 抽象句法(Abstract syntax): 抽象句法是一个规则的集合, 通常是公理系统(axiom system)的形式,或者是一个分类定义(sort definition)的集合形式,它定义了一个结构的集合且没有规定精确的外部世界或这些结构的计算机(即数据)表示
284. 形式(的)(Formal): 通过"形式的"在我们的上下文(即软件工程的上下文)中,我们指一个语言,系统,论证(推理方式),程序或规约,其句法和语义基于数学(包括数理逻辑)(的规则)
672. 规约(Specification): 我们使用术语"规约"来涵盖领域描述(domain description), 需求规定(requirements prescription)和软件设计(software design)的概念.特别地,规约通常是由许多定义(definition)构成的一个定义
参考文献
1. M. Abadi, L. Cardelli: A Theory of Objects (Springer, New York, USA 1996)
2. H. Abelson, G.J. Sussman, J. Sussman: Structure and Interpretation of Computer Programs (MIT Press, USA 1996)
3. J.-R. Abrial: The B Book: Assigning Programs to Meanings (Cambridge University Press, UK 1996)
4. J.-R. Abrial, L. Mussat. Event B Reference Manual (Editor: Thierry Lecomte),June 2001. Report of EU 1ST Project Matisse IST-1999-11435.
5. J.-R. Abrial, S.A. Schuman, B. Meyer: Specification Language. In: On theConstruction of Programs: An Advanced Course, ed by R.M. McKeag, A.M.Macnaghten (Cambridge University Press, 1980) pp 343-410
6. J.-R. Abrial, I.H. S0rensen: KWIC-index generation. In: Program Specification:Proceedings of a Workshop, vol 134 of Lecture Notes in Computer Science, ed by J. Staunstrup (Springer, 1981) pp 88-95
7. A. Aho, J. Hopcroft, J. Ullman: The Design of Computer Algorithms (AddisonWesley, USA 1974)
8. A.V. Aho, R. Sethi, J.D. Ullman: Compilers: Principles, Techniques, and Tools (Addison-Wesley, USA 1977, 1986)
9. R. Alur, D.L. Dill: A Theory of Timed Automata. Theoretical Computer Science 126, 2 (1994) pp 183-235
10. Edited by J. Alves-Foss: Formal Syntax and Semantics of Java (Springer, 1998)
11. D. Andrews, W. Henhapl: Pascal. In: [121] (Prentice Hall, 1982) pp 175-252
12. ANSI X3.23-1974: The COBOL Programming Language. Technical Report,American National Standards Institute, Standards on Computers and Information Processing (1974)
13. ANSI X3.53-1976: The PL/I Programming Language. Technical Report, American National Standards Institute, Standards on Computers and Information Processing (1976)
14. ANSI X3.9-1966: The FORTRAN Programming Language. Technical Report,American National Standards Institute, Standards on Computers and Information Processing (1966)
15. K. Apt: Ten Years of Roarers Logic: A Survey — Part I. ACM Trans, on Prog.Lang, and Systems 3 (1981) pp 431-483
16. K. Apt: Ten Years of Roarers Logic: A Survey — Part II: Nondeterminism.Theoretical Computer Science 28 (1984) pp 83-110
17. K.R. Apt: From Logic Programming to Prolog (Prentice Hall, 1997)
18. K.R. Apt: Principles of Constraint Programming (Cambridge University Press,August 2003)
19. K.R. Apt, E.-R. Olderog: Verification of Sequential and Concurrent Programs(Springer, 1997)
20. K. Arnold, J. Gosling, D. Holmes: The Java Programming Language (AddisonWesley, US 1996)
21. R.-J. Back, J. von Wright: Refinement Calculus: A Systematic Introduction(Springer, Heidelberg, 1998)
22. J.W. Backus: The Syntax and Semantics of the proposed International Algebraic Language of the Zurich ACM-GAMM Conference. In: ICIP Proceedings,Paris 1959 (Butterworth's, London, 1960) pp 125-132
23. J.W. Backus: Can Programming Be Liberated from the von Neumann Style?A Functional Style and Its Algebra of Programs. Communications of the ACM 21, 8 (1978) pp 613-641
24. J.W. Backus, P. Naur: Revised Report on the Algorithmic Language ALGOL 60. Communications of the ACM 6, 1 (1963) pp 1-1
25. H.P. Barendregt: The Type Free Lambda Calculus. In: [33] (North-Holland,Amsterdam, 1977) pp 1091-1132
26. H.P. Barendregt: The Lambda Caculus — Its Syntax and Semantics (NorthHolland, Amsterdam, 1981)
27. H.P. Barendregt: Introduction to Lambda Calculus. Niew Archief Voor Wiskunde 4 (1984) pp 337-372
28. H.P. Barendregt: Functional Programming and Lambda Calculus. In: [344] —vol.B., ed by J. Leeuwen (North-Holland, Amsterdam, 1990) pp 321-363
29. H.P. Barendregt: The Lambda Calculus, no 103 of Studies in Logic and the Foundations of Mathematics, revised edn (North-Holland, Amsterdam 1991)
30. Edited by J. Barnes: The Complete Works of Aristotle; I and II (PrincetonUniversity Press, NJ, USA 1984)
31. W. Barnstone: Border of a Dream: Selected Poems of Antonio Machado (Copper Canyon Press, WA, USA 2003)
32. H. Barringer, J. Cheng, C.B. Jones: A logic covering undefinedness in program proofs. Acta Informatica 21 (1984) pp 251-269
33. Edited by J. Barwise: Handbook of Mathematical Logic (North-Holland, Amsterdam, 1977)
34. F. Bauer, H. Wossner: Algorithmic Language and Program Development (Springer, 1982)
35. F.L. Bauer, M. Broy, editors. Program Construction, International Summer School, July 26-August 6, 1978, Marktoberdorf, Germany, volume 69 of Lecture Notes in Computer Science. Springer, 1979.
36. H. Bekic: Programming Languages and Their Definition. In: Lecture Notes in Computer Science, Vol. 177, ed by C.B. Jones (Springer, 1984)
37. H. Bekic, D. Bj0rner, W. Henhapl, C.B. Jones, P. Lucas: A Formal Definition of a PL/I Subset. Technical Report 25.139, Vienna, Austria (1974)
38. H. Bekic, P. Lucas, K. Walk, et al.: Formal Definition of PL/I, ULD VersionI. Technical Report, IBM Laboratory, Vienna (1966)
39. H. Bekic, P. Lucas, K. Walk, et al.: Formal Definition of PL/I, ULD VersionII. Technical Report, IBM Laboratory, Vienna (1968)
40. H. Bekic, P. Lucas, K. Walk, et al.: Formal Definition of PL/I, ULD VersionIII. IBM Laboratory, Vienna, 1969.
41. C. Berge: Theorie des Graphes et ses Applications (Dunod, Paris, 1958)
42. C. Berge: Graphs, vol 6 of Mathematical Library, second revised edition of part1 of the 1973 english version edn (North-Holland, 1985)
43. J. Bergstra, J. Heering, P. Klint: Algebraic Specification (Addison-Wesley,ACM Press, 1989)
44. E. Berlekamp, J. Conway, R. Guy: Winning Ways for Your Mathematical Plays, vol. 1 (Academic Press, 1982)
45. E. Berlekamp, J. Conway, R. Guy: Winning Ways for Your Mathematical Plays, vol. 2 (Academic Press, 1982)
46. P. Bernays: Axiomatic Set Theory (Dover, NY, USA 1991)
47. G. Berry. Proof, Language and Interaction: Essays in Honour of Robin Milner,chapter The Foundations of Esterel. MIT Press, 1998.
48. G. Berry, G. Gonthier: The Esterel Synchronous Programming Language: Design, Semantics, Implementation. Science of Computer Programming 19, 2(1992) pp 87-152
49. M. Bidoit, P.D. Mosses: CASL User Manual (Springer, 2004)
50. R. Bird, O. de Moor: Algebra of Programming (Prentice Hall, September 1996)
51. R.S. Bird, P. Wadler: Introduction to Functional Programming (Prentice Hall,1988)
52. G. Birkhoff: Lattice Theory, 3 edn (American Mathematical Society, Providence, RI 1967)
53. G. Birkhoff, S. MacLane: A Survey of Modern Algebra (Macmillan, 1956)
54. G. Birtwistle, O.-J.Dahl, B. Myhrhaug, K. Nygaard: SIMULA begin (Studentlitteratur, Sweden, 1974)
55. D. Bj0rner: Programming Languages: Formal Development of Interpreters and Compilers. In: International Computing Symposium 77 (North-Holland, Amsterdam, 1977) pp 1-21
56. D. Bj0rner: Programming Languages: Linguistics and Semantics. In: International Computing Symposium 77 (North-Holland, Amsterdam, 1977) pp 511-536
57. D. Bj0rner: Programming in the Meta-Language: A Tutorial. In: The Vienna Development Method: The Meta-Language, [120], ed by D. Bj0rner, C.B. Jones (Springer, 1978) pp 24-217
58. D. Bj0rner: Software Abstraction Principles: Tutorial Examples of an Operating System Command Language Specification and a PL/I-like OnCondition Language Definition. In: The Vienna Development Method: The Meta-Language, [120], ed by D. Bj0rner, C.B. Jones (Springer, 1978) pp 337-374
59. D. Bj0rner: The Systematic Development of a Compiling Algorithm. In: LePoint sur la Compilation, ed by Amirchahy, Neel (INRIA, Paris, 1979) pp45-88
60. D. Bj0rner: The Vienna Development Method: Software Abstraction and Program Synthesis. In: Mathematical Studies of Information Processing, vol 75 of LNCS (Springer, 1979)
61. Edited by D. Bj0rner: Abstract Software Specifications, vol 86 of LNCS (Springer, 1980)
62. D. Bj0rner: Application of Formal Models. In: Data Bases (INFOTECH Proceedings, 1980)
63. D. Bj0rner: Experiments in Block-Structured GOTO-Modelling: Exits vs. Continuations. In: Abstract Software Specification, [61], vol 86 of LNCS, ed by D.Bj0rner (Springer, 1980) pp 216-247
64. D. Bj0rner: Formal Description of Programming Concepts: a Software Engineering Viewpoint. In: MFCS'80, Lecture Notes Vol 88 (Springer, 1980) pp1-21
65. D. Bj0rner: Formalization of Data Base Models. In: Abstract Software Specification, [61], vol 86 of LNCS, ed by D. Bj0rner (Springer, 1980) pp 144-215
66. D. Bj0rner: The VDM Principles of Software Specification and Program Design.In: TC2 Work. Confi on Formalisation of Programming Concepts, Peniscola,Spain (Springer, LNCS Vol. 107 1981) pp 44-74
67. D. Bj0rner: Realization of Database Management Systems. In: See [121] (Prentice Hall, 1982) pp 443-456
68. D. Bj0rner: Rigorous Development of Interpreters and Compilers. In: See [121](Prentice Hall, 1982) pp 271-320
69. D. Bj0rner: Stepwise Transformation of Software Architectures. In: See [121](Prentice Hall, 1982) pp 353-378
70. D. Bj0rner: Software Architectures and Programming Systems Design. Vols.I-VI. Techn. Univ. of Denmark (1983-1987)
71. D. Bj0rner: Project Graphs and Meta-Programs: Towards a Theory of Software Development. In: Proc. Capri '86 Conf. on Innovative Software Factories andAda, Lecture Notes on Computer Science, ed by N. Habermann, U. Montanari(Springer, 1986)
72. D. Bj0rner: Software Development Graphs — A Unifying Concept for Software Development? In: Vol. 241 of Lecture Notes in Computer Science: Foundations of Software Technology and Theoretical Computer Science, ed by K. Nori(Springer, 1986) pp 1-9
73. D. Bj0rner: Software Engineering and Programming: Past-Present-Future.IPSJ: Inform. Proc. Soc. of Japan 8, 4 (1986) pp 265-270
74. D. Bj0rner: On the Use of Formal Methods in Software Development. In:Proc. of 9th International Conf. on Software Engineering, Monterey, California(1987) pp 17-29
75. D. Bj0rner: The Stepwise Development of Software Development Graphs:Meta-Programming VDM Developments. In: See [122], vol 252 of LNCS(Springer, Heidelberg, 1987) pp 77-96
76. D. Bj0rner: Facets of Software Development: Computer Science & Programming, Engineering & Management. J. of Comput. Sci. h Techn. 4, 3 (1989) pp193-203
77. D. Bj0rner: Specification and Transformation: Methodology Aspects of the Vienna Development Method. In: TAPSOFT'89, vol 352 of Lecture Notes in Computer Science (Springer, Heidelberg, 1989) pp 1-35
78. D. Bj0rner: Formal Software Development: Requirements for a CASE. In: European Symposium on Software Development Environment and CASE Technology, Konigswinter, FRG, June 17-21 (Springer, Heidelberg, 1991)
79. D. Bj0rner: Formal Specification Is an Experimental Science (in English). In: Intl. Conf. on Perspectives of System Informatics (1991)
80. D. Bj0rner: Formal Specification Is an Experimental Science (in Russian). Programmirovanie 6 (1991) pp 24-43
81. D. Bj0rner: Towards a Meaning of 'M' in VDM. In: Formal Description of Programming Concepts, ed by E. Neuhold, M. Paul (Springer, Heidelberg, 1991) pp 137-258
82. D. Bj0rner: Prom Research to Practice: Self-reliance of the Developing World Through Software Technology: Usage, Education & Training, Development & Research, pp 65-71. In: Information Processing '92, IFIP World Congress '92,Madrid, ed by J. van Leeuwen (IFIP Transaction A-12: Algorithms, Software,Architecture, North-Holland 1992)
83. D. Bj0rner: Trustworthy Computing Systems: The ProCoS Experience. In:14'th ICSE: Intl. Conf. on Software Eng., Melbourne, Australia (ACM Press,1992) pp 15-34
84. D. Bj0rner. Formal Models of Robots: Geometry & Kinematics, chapter 3,pages 37-58. Eds.: W. Roscoe and J. Woodcock, A Classical Mind, Festschrift for C.A.R. Hoare. Prentice Hall, January 1994.
85. D. Bj0rner: Prospects for a Viable Software Industry — Enterprise Models, Design Calculi, and Reusable Modules. In: First ACM Japan Chapter Conference(World Scientific, Singapore 1994)
86. D. Bj0rner: Software Systems Engineering — From Domain Analysis to Requirements Capture: An Air Traffic Control Example. In: 2nd Asia-Pacific Software Engineering Conference (APSEC '95) (IEEE Computer Society, 1995)
87. D. Bj0rner: From Domain Engineering via Requirements to Software. Formal Specification and Design Calculi. In: SOFSEM'97, vol 1338 of Lecture Notes in Computer Science (Springer, 1997) pp 219-248
88. D. Bj0rner: Challenges in Domain Modelling — Algebraic or Otherwise. Research, Department of Information Technology, Technical University of Denmark, Denmark (1998)
89. D. Bj0rner: Domains as Prerequisites for Requirements and Software &c. In:RTSE'97: Requirements Targeted Software and Systems Engineering, vol 1526of Lecture Notes in Computer Science, ed by M. Broy, B. Rumpe (Springer,Heidelberg 1998) pp 1-41
90. D. Bj0rner: Formal Methods in the 21st Century — An Assessment of Today,Predictions for The Future — Panel position presented at the ICSE'98, Kyoto,Japan. Technical Report, Department of Information Technology, TechnicalUniversity of Denmark (1998)
91. D. Bj0rner: Issues in International Cooperative Research — Why Not Asian,African or Latin American 'Esprits'? Research, Department of InformationTechnology, Technical University of Denmark, DK-2800 Lyngby, Denmark(1998)
92. D. Bj0rner: A Triptych Software Development Paradigm: Domain, Requirements and Software. Towards a Model Development of a Decision Support System for Sustainable Development. In: Festschrift to Hans Langmaack: Correct Systems Design: Recent Insight and Advances, vol 1710 of Lecture Notes in Computer Science, ed by E.-R. Olderog, B. Steffen (Springer, 1999) pp 29-60
93. D. Bj0rner: Challenge 2000: some aspects of: "How to Create a Software Industry". In: Proceedings of CSIC'99, Ed.: R. Jalili (1999)
94. D. Bj0rner: Where Do Software Architectures Come from? Systematic Development from Domains and Requirements. A Re-assessment of Software Engineering? South African Journal of Computer Science 22 (1999) pp 3-13
95. D. Bj0rner: Domain Engineering, A Software Engineering Discipline in Need of Research. In: SOFSEM'2000: Theory and Practice of Informatics, vol 1963 of Lecture Notes in Computer Science (Springer) pp 1-17
96. D. Bj0rner: Domain Modelling: Resource Management Strategics, Tactics &Operations, Decision Support and Algorithmic Software. In: Millennial Perspectives in Computer Science, ed by J. Davies, B. Roscoe, J. Woodcock (Palgrave, UK 2000) pp 23-40
97. D. Bj0rner: Formal Software Techniques in Railway Systems. In: 9th IFAC Symposium on Control in Transportation Systems, ed by E. Schnieder (DVI2000) pp 1-12
98. D. Bj0rner: Informatics: A Truly Interdisciplinary Science — Computing Science and Mathematics. In: 9th Intl. Colloquium on Numerical Analysis and Computer Science with Applications, ed by D. Bainov (Academic Publications, Bulgaria 2000)
99. D. Bj0rner: Informatics: A Truly Interdisciplinary Science — Prospects for an Emerging World. In: Information Technology and Communication — at the Dawn of the New Millennium, ed by S. Balasubramanian (AIT Press, 2000)pp 71-84
100. D. Bj0rner: Pinnacles of Software Engineering: 25 Years of Formal Methods. Annals of Software Engineering 10 (2000) pp 11-66
101. D. Bj0rner: Informatics Models of Infrastructure Domains. In: Computer Science and Information Technologies (Institute for Informatics and Automation Problems, Yerevan, Armenia 2001) pp 13-73
102. D. Bj0rner: On Formal Techniques in Protocol Engineering: Example Challenges. In: Formal Techniques for Networks and Distributed Systems (Eds.:Myungchul Kim, Byoungmoon Chin, Sungwon Kang and Danhyung Lee) (Kluwer, 2001) pp 395-420
103. D. Bj0rner: Some Thoughts on Teaching Software Engineering - Central Roles of Semantics. In: Liber Amicorum: Professor Jaco de Bakker (Stichting Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands 2002) pp27-45
104. D. Bj0rner: Domain Engineering: A "Radical Innovation" for Systems and Software Engineering? In: Verification: Theory and Practice, vol 2772 of Lecture Notes in Computer Science (Springer, Heidelberg 2003)
105. D. Bj0rner: Dynamics of Railway Nets: On an Interface Between Automatic Control and Software Engineering. In: CTS2003: 10th IFAC Symposium on Control in Transportation Systems (Elsevier Science, Oxford, UK 2003)
106. D. Bj0rner: Logics of Formal Software Specification Languages — The Possible Worlds cum Domain Problem. In: Fourth Pan-Hellenic Symposium on Logic, ed by L. Kirousis (Univ. of Thessaloniki, 2003)
107. D. Bj0rner: New Results and Trends in Formal Techniques for the Development of Software for Transportation Systems. In: FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems (Institutfur Verkehrssicherheit und Automatisierungstechnik, Techn. Univ. of Braunschweig, Germany, 2003)
108. D. Bj0rner. 'What Is a Method?" — An Essay on Some Aspects of Software Engineering, chapter 9, pages 175-203. Monographs in Computer Science. IFIP: International Federation for Information Processing. Springer, NY, USA,2003. Programming Methodology: Recent Work by Members of IFIP Working Group 2.3. Eds.: Annabelle Mclver and Carroll Morgan.
109. D. Bj0rner: What Is an Infrastructure? In: Formal Methods at the Crossroads.From Panacea to Foundational Support (Springer, Heidelberg, Germany 2003)
110. D. Bj0rner: Towards "Posit & Prove" Design Calculi for Requirements Engineering and Software Design. In: From Object- Orientation to Formal Methods- Essays in Memory of Ole-Johan Dahl, Lecture Notes in Computer Science,Vol. 2635 (Springer, 2004)
111. D. Bj0rner: Domain Engineering: "Upstream" from Requirements Engineering and Software Design. US ONR + Univ. of Genoa Workshop, Santa Margherita Ligure (June 2000)
112. D. Bj0rner, J.R. Cuellar: Software Engineering Education: Roles of Formal Specification and Design Calculi. Annals of Software Engineering 6 (1998) pp365-410
113. D. Bj0rner, Y.L. Dong, S. Prehn: Domain Analyses: A Case Study of Station Management. In: KICS'94: Kunming International CASE Symposium, Yunnan Province, China (1994)
114. D. Bj0rner, L. Druffel: Industrial Experience in Using Formal Methods. In:Intl. Conf. on Software Engineering (IEEE Computer Society Press, 1990) pp264-266
115. Edited by D. Bj0rner, A. Ershov, N. Jones: Partial Evaluation and Mixed Computation. Proceedings of the IFIP TC2 Workshop, Gammel Avernces, Denmark,October 1987 (North-Holland, 1988)
116. D. Bj0rner, C. George, S. Prehn. Scheduling and Rescheduling of Trains, chapter 8, pages 157-184. Industrial Strength Formal Methods in Practice, Eds.:Michael G. Hinchey and Jonathan P. Bowen. FACIT, Springer, London, England, 1999.
117. D. Bj0rner, C.W. George, A.E. Haxthausen et al.: "UML"-ising Formal Techniques. In: INT 2004: Third International Workshop on Integration of Specification Techniques for Applications in Engineering, vol 3147 of Lecture Notesin Computer Science (Springer, 2004, ETAPS, Barcelona, Spain) pp 423-450
118. D. Bj0rner, C.W. George, S. Prehn: Computing Systems for Railways — A Rolefor Domain Engineering. Relations to Requirements Engineering and Softwarefor Control Applications. In: Integrated Design and Process Technology. Editors: Bernd Kraemer and John C. Petterson (Society for Design and ProcessScience, Texas, USA 2002)
119. D. Bj0rner, A.E. Haxthausen, K. Havelund: Formal, Model-Oriented SoftwareDevelopment Methods: From VDM to ProCoS, and from RAISE to LaCoS.Future Generation Computer Systems (North-Holland, 1992)
120. Edited by D. Bj0rner, C. Jones: The Vienna Development Method: The MetaLanguage, vol 61 of LNCS (Springer, 1978)
121. Edited by D. Bj0rner, C. Jones: Formal Specification and Software Development(Prentice Hall, 1982)
122. D. Bj0rner, C. Jones, M.M. an Airchinnigh, E. Neuhold, editors. VDM -A Formal Method at Work. Proc. VDM-Europe Symposium 1987, Brussels,Belgium, Springer, Lecture Notes in Computer Science, Vol. 252, 1987.
123. D. Bj0rner, S. Koussobe, R. Noussi, G. Satchok: Michael Jackson's ProblemFrames: Towards Methodological Principles of Selecting and Applying Formal Software Development Techniques and Tools. In: ICFEM'91: Intl. Conf.on 'Formal Engineering Methods", Hiroshima, Japan, ed by L. ShaoQi, M.Hinchley (IEEE Computer Society Press, CA, USA 1997) pp 263-271
124. D. Bj0rner, H.H. L0vengreen: Formal Semantics of Data Bases. In: 8th InVl.Very Large Data Base Conf. (VLDB Found. 1982)
125. D. Bj0rner, H.H. L0vengreen: Formalization of Data Models. In: Formal Specification and Software Development, [121] (Prentice Hall, 1982) pp 379-442
126. D. Bj0rner, M. Nielsen: Meta Programs and Project Graphs. In: ETW: EspritTechnical Week (Elsevier, 1985) pp 479-491
127. D. Bj0rner, J. Nilsson: Algorithmic & Knowledge Based Methods — Do They"Unify"? — with Some Programme Remarks for UNU/IIST. In: InternationalConference on Fifth Generation Computer Systems: FGCS'92 (ICOT, 1992)pp (Separate folder, "191-198")
128. Edited by D. Bj0rner, O. Oest: Towards a Formal Description of Ada, vol 98of LNCS (Springer, 1980)
129. D. Bj0rner, O.N. Oest: The DDC Ada Compiler Development Project. In:Towards a Formal Description of Ada, [128], vol 98 of LNCS, ed by D. Bj0rner,O.N. Oest (Springer, 1980) pp 1-19
130. D. Bj0rner, S. Prehn: Software Engineering Aspects of VDM. In: Theory andPractice of Software Technology, ed by D. Ferrari (North-Holland, Amsterdam,1983)
131. A. Blikle: MetaSoft Primer; Towards a Metalanguage for Applied DenotationalSemantics, vol 288 of Lecture Notes in Computer Science (Springer, 1987)
132. A. Blikle: A Guided Tour of the Mathematics of MetaSoft. Information Processing Letters 29 (1988) pp 81-86
133. A. Blikle: Three-valued predicates for software specification and validation.In: [135] (1988) pp 243-266
134. W.D. Blizard: A Formal Theory of Objects, Space and Time. The Journal ofSymbolic Logic 55, 1 (1990) pp 74-89
135. R. Bloomfield, L. Marshall, R. Jones, editors. VDM - The Way Ahead. Proc.2nd VDM-Europe Symposium 1988, Dublin, Ireland, Springer, Lecture Notesin Computer Science, Vol. 328, September 1988.
136. G.S. Boolos, R.C. Jeffrey: Computability and Logic (Cambridge UniversityPress, September 29, 1989)
137. J.P. Bowen: Glossary of Z Notation. Information and Software Technology 37,5-6 (1995) pp 333-334
138. British Standards Institution: Specification for Computer Programming Language Pascal. Technical Report BS6192, BSI (1982)
139. M. Broy, K. St0len: Specification and Development of Interactive Systems —Focus on Streams, Interfaces and Refinement (Springer, NY, USA and Heidelberg, Germany 2001)
140. R. Bruni, J. Meseguer: Generalized Rewrite Theories. In: Automata, Languagesand Programming. 30th International Colloquium, ICALP 2003, Eindhoven,The Netherlands, June 30-July 4, 2003. Proceedings, vol 2719 of Lecture Notesin Computer Science, ed by J.CM. Baeten, J.K.Lenstra, J.Parrow, G.J. Woeginger (Springer, 2003) pp 252-266
141. E. Burke: Reflections on the Revolution in France, Ed. Conor Cruise O'Brien(Hammondsworth, 1790 (1968))
142. R.M. Burstall, J. Darlington: A Transformation System for Developing Recursive Programs. Journal of ACM 24, 1 (1977) pp 44-67
143. D. Cansell, D. Mery: Logical Foundations of the B Method. Computing andInformatics 22, 1-2 (2003)
144. D. Carrington, D.J. Duke, R. Duke et al.: Object-Z: An Object-Oriented Extension to Z. In: Formal Description Techniques, II (FORTE,89), ed by S.Vuong (Elsevier — (North-Holland), 1990) pp 281-296
145. C.C.I.T.T.: The Specification of CHILL. Technical Report Recommendation Z200, International Telegraph and Telephone Consultative Committee,Geneva, Switzerland (1980)
146. E. Chailloux, P. Manoury, B. Pagano: Developing Applications With ObjectiveCaml (Project Cristal, INRIA, France 2004)
147. E. Chailloux, P. Manoury, B. Pagano: Developpement a1'applications avec Objective Caml (Editions O'Reilly, Paris, France 2000)
148. P.P. Chen: The Entity-Relationship Model — Toward a Unified View of Data.ACM Trans. Database Syst 1, 1 (1976) pp 9-36
149. P.P. Chen, editor. Entity-Relationship Approach to Systems Analysis and Design. Proc. 1st International Conference on the Entity-Relationship Approach.North-Holland, 1980.
150. J. Cheng: A Logic for Partial Functions. PhD Thesis, Department of ComputerScience, University of Manchester (1986)
151. J. Cheng, C. Jones: On the usability of logics which handle partial functions. In:Proceedings of the Third Refinement Workshop, ed by C. Morgan, J. Woodcock(Springer, 1990)
152. A. Church: The Calculi of Lambda-Conversion, vol 6 of Annals of MathematicalStudies (Princeton University Press, USA 1941)
153. A. Church: Introduction to Mathematical Logic (Princeton University Press,USA 1956)
154. M. Clavel, F. Duran, S. Eker et al: The Maude 2.0 System. In: Rewriting Techniques and Applications (RTA 2003), no 2706 of Lecture Notes in ComputerScience, ed by Robert Nieuwenhuis (Springer, 2003) pp 76-87
155. G. Clemmensen, O. Oest: Formal Specification and Development of an AdaCompiler - A VDM Case Study. In: Proc. 7th International Conf. on SoftwareEngineering, 26.-29. March 1984, Orlando, Florida (IEEE Press, 1984) pp430-440
156. E.F. Codd: A Relational Model For Large Shared Databank. Communicationsof the ACM 13, 6 (1970) pp 377-387
157. P. Cohn: Universal Algebra, rev. edn ((Harper and Row) D. Reidel, Boston(1965) 1981)
158. P. Cohn: Classical Algebra (Wiley, 2001)
159. J. Conway: On Numbers and Games (Academic Press, 1976)
160. D. Cooper: The Equivalence of Certain Computations. Computer Journal 9(1966) pp 45-52
161. T.H. Cormen, C.E. Leiserson, R.L. Rivest, C. Stein: Introduction to Algorithms,2nd edn (McGraw-Hill and MIT Press, 2001)
162. G. Cousineau, M. Mauny: The Functional Approach to Programming (Cambridge University Press, UK 1998)
163. P. Cousot: Abstract Interpretation. ACM Computing Surveys 28, 2 (1996) pp324-328
164. P. Cousot, R. Cousot: Abstract Interpretation: A Unified Lattice Model forStatic Analysis of Programs by Construction or Approximation of Fixpoints.In: 4th POPL: Principles of Programming and Languages (ACM Press, 1977)pp 238-252
165. D. Crystal: The Cambridge Encyclopedia of Language (Cambridge UniversityPress, 1987, 1988)
166. H.B. Curry, R. Feys: Combinatory Logic I (North-Holland, Amsterdam, 1968)
167. H.B. Curry, J.R. Hindley, J.P. Seldin: Combinatory Logic II (North-Holland,Amsterdam, 1972)
168. O.-J. Dahl, E.W. Dijkstra, C.A.R. Hoare: Structured Programming (AcademicPress, 1972)
169. O.-J. Dahl, C.A.R. Hoare: Hierarchical Program Structures. In: [168] (Academic Press, 1972) pp 197-220
170. O.-J. Dahl, K. Nygaard: SIMULA - An ALGOL-based Simulation Language.Communications of the ACM 9, 9 (1966) pp 671-678
171. W. Damm, D. Harel: LSCs: Breathing Life into Message Sequence Charts.Formal Methods in System Design 19 (2001) pp 45-80
172. O. Danvy: A Rational Deconstruction of Landin's SECD Machine. ResearchRS 03-33, BRICS: Basic Research in Computer Science, University of Arhus,Denmark (2003)
173. J. Darlington: A Synthesis of Several Sorting Algorithms. Acta Informatica 11(1978) pp 1-30
174. J. Darlington, R.M. Burstall: A System Which Automatically Improves Programs. Acta Informatica 6 (1976) pp 41-60
175. J. Darlington, P. Henderson, D. Turner: Functional Programming and Its Applications (Cambridge Univ. Press, 1982)
176. C. Date: An Introduction to Database Systems, I (Addison-Wesley, 1981)
177. C. Date: An Introduction to Database Systems, II (Addison-Wesley, 1983)
178. C. Date, H. Darwen: A Guide to the SQL Standard (Addison-Wesley Professional, November 8, 1996)
179. J. Davies. Announcement: Electronic version of Communicating SequentialProcesses (CSP). Published electronically: http://www.usingcsp.com/, 2004.Announcing revised edition of [288].
180. M. Davis: Computability and Undecidability (McGraw-Hill, 1958)181. R.E. Davis: Truth, Deduction, and Computation (Computer Science Press, NewYork, USA 1989)
182. J. de Bakker: Mathematical Theory of Programming Correctness (Prentice Hall,1980)
183. J. de Bakker: Control Flow Semantics (MIT Press, USA, 1995)
184. N. Dershowitz, J.-P. Jouannaud: Rewrite Systems. In: Handbook of TheoreticalComputer Science, Volume B: Formal Models and Semantics, ed by J. vanLeeuwen (Elsevier, 1990) pp 243-320
185. R. Descartes: Discours de la methode pour bien conduire sa raison et chercherla verite dans les sciences, with three appendices: La Dioptrique, Les Met cores,and La Geometrie (Leyden, The Netherlands 1637)
186. R. Descartes: La Geometrie (France, 1637)
187. R. Descartes: Discourse on Method and Related Writings (from: Discourse onthe Method of Rightly Conducting the Reason, and Seeking Truth in the Sciences) (France and Penguin Classics, 1637, respectively February 28, 2000)
188. R. Descartes: Discourse on Method and Related Writings (Penguin Classics,2000)
189. R. Descartes: Discourse on Method, Optics, Geometry, and Meteorology (Hackett Publishing Co, Cambridge, USA 2001)
190. R. Diaconescu, K. Futatsugi: Logical Semantics of CafeOBJ. Research ReportIS-RR-96-0024S, JAIST, Japan (1996)
191. R. Diaconescu, K. Futatsugi: CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification (WorldScientific, Singapore, 1998)
192. R. Diaconescu, K. Futatsugi, S. Iida: CafeOBJ Jewels. In: CAFE: AnIndustrial-Strength Algebraic Formal Method (Elsevier, 2000) pp 33-60
193. R. Diaconescu, K. Futatsugi, K. Ogata: CafeOBJ: Logical Foundations andMethodology. Computing and Informatics 22, 1-2 (2003)
194. E. Dijkstra: A Discipline of Programming (Prentice Hall, 1976)
195. E. Dijkstra, W. Feijen: A Method of Programming (Addison-Wesley, 1988)
196. E. Dijkstra, C. Scholten: Predicate Calculus and Program Semantics (Springer,1990)
197. O. Dommergaard: The Design of a Virtual Machine for Ada. In: [61] (Springer,1980) pp 463-605
198. O. Dommergaard, S. Bodilsen: A Formal Definition of P-Code. Technical Report, Dept. of Comp. Sci., Techn. Univ. of Denmark (1980)
199. D.J. Duke, R. Duke: Towards a Semantics for Object-Z. In: VDM and Z - Formal Methods in Software Development, vol 428 of Lecture Notes in ComputerScience, ed by D. Bj0rner, C.A.R. Hoare, H. Langmaack (Springer, 1990) pp244-261
200. R. Duke, P. King, G.A. Rose, G. Smith: The Object-Z Specification Language.In: Technology of Object-Oriented Languages and Systems: TOOLS 5, ed byT. Korson et al. (Prentice Hall, 1991) pp 465-483
201. E.H. Diirr, L. Dusink: Role of VDM(++) in the Development of a Real-TimeTracking and Tracing System. In: FMEy9S: Industrial-Strength Formal Methods, ed by J. Woodcock, P. Larsen (Springer, 1993) pp 64-72
202. E.H. Diirr, S. Goldsack. Formal Methods and Object Technology, chapter 6Concurrency and Real-Time in VDM++, pages 86-112. Springer (Eds. S.J.Goldsack and S.J.H. Kent), London, 1996.
203. E.H. Diirr, J. van Katwijk: V D M + + - A Formal Specification Language forObject-Oriented Designs. In: Technology of Object-oriented Languages and Systems, ed by B.M. Heeg, B. Magnusson (Prentice Hall, 1992) pp 63-78
204. E.H. Diirr, W. Lourens, J. van Katwijk: The Use of the Formal Specification Language V D M + + for Data Acquisition Systems. In: New ComputingTechniques in Physics Research II, ed by D. Perret-Gallix (World Scientific,Singapore 1992) pp 47-52
205. B. Dutertre: Complete Proof System for First-Order Interval Temporal Logic.In: Proceedings of the 10th Annual IEEE Symposium on Logic in ComputerScience (IEEE CS, 1995) pp 36-43
206. R.K. Dybvig: The Scheme Programming Language (MIT Press, Cambridge,USA 2003)
207. Encyclopaedia Brittanica. Encyclopaedia Brittanica. MerriamWebster/Brittanica: Access over the Web: http://www.eb.com: 180/, 1999.
208. H. Ehrig, B. Mahr: Fundamentals of Algebraic Specification 1, Equations andInitial Semantics (EATCS Monographs on Theoretical Computer Science, vol.6, Springer, 1985)
209. H. Ehrig, B. Mahr: Fundamentals of Algebraic Specification 2, Module Specifications and Constraints (EATCS Monographs on Theoretical Computer Science,vol. 21, Springer, 1990)
210. H.B. Enderton: A Mathematical Introduction to Logic (Academic Press, NewYork, 1974)
211. H.B. Enderton: Elements of Set Theory (Elsevier, Amsterdam, The Netherlands 23 May 1977)
212. E. Engeler: Symposium on Semantics of Algorithmic Languages, vol 188 ofLecture Notes in Mathematics (Springer, 1971)
213. S.S. Epp: Discrete Matematics with Applications, third edn (Thomson,*s/Cole, California, USA 2004)
214. A. Ershov: On the Essence of Translation. Computer Software and SystemProgramming 3, 5 (1977) pp 332-346
215. A. Ershov: On the Partial Computation Principle. Information Processing Letters 6, 2 (1977) pp 38-41
216. A. Ershov: Mixed Computation: Potential Applications and Problems for Study.Theoretical Computer Science 18 (1982) pp 41-67
217. A. Ershov: On Futamura Projections. BIT (Japan) 12, 14 (1982) pp 4-5
218. A. Ershov: On Mixed Computation: Informal Account of the Strict and Polyvariant Computational Schemes. In: Control Flow and Data Flow: Conceptsof Distributed Programming. NATO ASI Series F: Computer and System Sciences, vol. 14, ed by M. Broy Springer, 1985) pp 107-120
219. A. Ershov, D. Bj0rner, Y. Futamura et al., editors. Special Issue: SelectedPapers from the Workshop on Partial Evaluation and Mixed Computation,1987 (New Generation Computing, vol. 6, nos. 2,3). Ohmsha and Springer,1988.
220. A. Ershov, V. Grushetsky: An Implementation-Oriented Method for DescribingAlgorithmic Languages. In: Information Processing 77, Toronto, Canada, edby B. Gilchrist (North-Holland, 1977) pp 117-122
221. A. Ershov, V. Itkin: Correctness of Mixed Computation in Algol-like Programs. In: Mathematical Foundations of Computer Science, Tatranskd Lomnica, Czechoslovakia. (Lecture Notes in Computer Science, vol. 53), ed by J.Gruska (Springer, 1977) pp 59-77
222. A. Evans Jr.: The Lambda-Calculus and Its Relation to Programming Languages. Unpubl. Notes, MIT (1972)
223. R. Fagin, J.Y. Halpern, Y. Moses, M.Y. Vardi: Reasoning About Knowledge(MIT Press 1996)
224. W. Feijen, A. van Gasteren, D. Gries, J. Misra, editors. Beauty Is Our Business, Texts and Monographs in Computer Science, New York, NY, USA, 1990.Springer. A Birthday Salute to Edsger W. Dijkstra.
225. A. Field, P. Harrison: Functional Programming (Addison-Wesley, 1988)
226. J.S. Fitzgerald, P.G. Larsen: Developing Software Using VDM-SL (CambridgeUniversity Press, UK 1997)
227. FOLDOC: The free online dictionary of computing. Electronically, on the Web:http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?ISWIM, 2004.
228. P. Folkjaer, D. Bj0rner: A Formal Model of a Generalised CSP-like Language.In: Proc. IFIP>80, ed by S. Lavington (North-Holland, Amsterdam, 1980) pp95-99
229. Formal Systems Europe. Home of the FDR2. Published on the Internet:http://www.fsel.com/, 2003.
230. A. Fraenkel, Y. Bar-Hillel, A. Levy: Foundations of Set Theory, 2nd revisededn (Elsevier Science, Amsterdam, The Netherlands 1973)
231. Y. Futamura: Partial Evaluation of Computation Process - An Approach to aCompiler-Compiler. Systems, Computers, Controls 2, 5 (1971) pp 45-50
232. K. Futatsugi, R. Diaconescu: CafeOBJ Report — The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification (WorldScientific, Singapore 1998)
233. K. Futatsugi, J. Goguen, J.-P. Jouannaud, J. Meseguer: Principles of OBJ-2.In: 12th Ann. Symp. on Principles of Programming (ACM, 1985) pp 52-66
234. K. Futatsugi, A. Nakagawa, T. Tamai, editors. CAFE: An Industrial-StrengthAlgebraic Formal Method, Proceedings from an April 1998 Symposium, Numazu, Japan, Elsevier 2000
235. J. Gallier: Logic for Computer Science: Foundations of Automatic TheoremProving (Harper and Row, NY, USA, 1986)
236. C.W. George, P. Haff, K. Havelund et al: The RAISE Specification Language(Prentice Hall, UK 1992)
237. C.W. George, A.E. Haxthausen: The Logic of the RAISE Specification Language. Computing and Informatics 22, 1-2 (2003)
238. C.W. George, A.E. Haxthausen, S. Hughes et al: The RAISE Method (PrenticeHall, UK 1995)
239. C.W. George, H.D. Van, T. Janowski, R. Moore: Case Studies Using the RAISEMethod (Springer, London 2002)
240. C. Ghezzi, M. Jazayeri, D. Mandrioli: Fundamentals of Software Engineering(Prentice Hall, 2002)
241. J.-Y. Girard, Y. Lafont, P. Taylor: Proofs and Types, vol 7, Cambridge Tractsin Theoretical Computer Science edn (Cambridge Univ. Press, UK 1989)
242. Edited by M.J.C. Gordon, T.F. Melham: Introduction to HOL: A TheoremProving Environment for Higher-Order Logic (Cambridge University Press,UK 1993)
243. J. Gosling, F. Yellin: The Java Language Specification (ACM Press, 1996)
244. D. Gries: Compiler Construction for Digital Computers (Wiley, NY, 1971)
245. D. Gries: The Science of Programming (Springer, 1981)
246. D. Gries, F.B. Schneider: A Logical Approach to Discrete Math (Springer, 1993)
247. O. Grillmeyer: Exploring Computer Science with Scheme (Springer, New York,USA 1998)
248. P.L. Guernic, M.L. Borgne, T. Gauthier, C.L. Maire: Programming Real TimeApplications with Signal. In: Another Look at Real Time Programming, volSpecial Issue of Proceedings of the IEEE (1991)
249. I. Guessarian: Algebraic Semantics (Springer, 1981)
250. C. Gunter, J. Mitchell: Theoretical Aspects of Object-Oriented Programming(MIT Press, USA, 1994)
251. C. Gunter, D. Scott: Semantic Domains. In: [344] — v°l- B.: ed by J. Leeuwen(North-Holland, Amsterdam, 1990) pp 633-674
252. C. Gunther: Semantics of Programming Languages (MIT Press, USA, 1992)
253. Y. Gurevich: Sequential Abstract State Machines Capture Sequential Algorithms. ACM Transactions on Computational Logic 1, 1 (2000) pp 77-111
254. Edited by P. Haff: The Formal Definition of CHILL (ITU (Intl. Telecom.Union), Geneva, Switzerland 1981)
255. P. Haff, A. Olsen: Use of VDM Within CCITT. In: [122] (Springer, 1987) pp324-330
256. N. Halbwachs, P. Caspi, Pilaud: The Synchronous Dataflow Programming Language Lustre. In: Another Look at Real Time Programming, vol Special Issueof Proceedings of the IEEE (1991)
257. P. Hall, D. Bj0rner, Z. Mikolajuk: Decision Support Systems for SustainableDevelopment: Experience and Potential — a Position Paper. AdministrativeReport 80, UNU/IIST, Macau (1996)
258. P.R. Halmos: Naive Set Theory (Springer, Heidelberg, 1998)
259. A. Hamilton: Logic for Mathematicians (Cambridge University Press, 1978,revised ed.: 1988)
260. A. Hamilton: Numbers, Sets and Axioms: the Apparatus of Mathematics (Cambridge University Press, 1982)
261. M.R. Hansen, H. Rischel: Functional Programming in Standard ML (AddisonWesley, 1997)
262. S. Harbinson: Modula 3 (Prentice Hall, USA 1992)
263. G. Hardy: A Course of Pure Mathematics (Cambridge University Press, England, 1908, 1943-4, 1949)
264. D. Harel: Algorithmics —The Spirit of Computing (Addison-Wesley, 1987)
265. D. Harel: Statecharts: A Visual Formalism for Complex Systems. Science ofComputer Programming 8, 3 (1987) pp 231-274
266. D. Harel: On Visual Formalisms. Communications of the ACM 33, 5 (1988)
267. D. Harel: The Science of Computing — Exploring the Nature and Power ofAlgorithms (Addison-Wesley, April 1989)
268. D. Harel, E. Gery: Executable Object Modeling with Statecharts. IEEE Computer 30, 7 (1997) pp 31-42
269. D. Harel, H. Lachover, A. Naamad et al: STATEMATE: A Working Environment for the Development of Complex Reactive Systems. Software Engineering16, 4 (1990) pp 403-414
270. D. Harel, R. Marelly: Come, Let's Play - Scenario-Based Programming UsingLSCs and the Play-Engine (Springer, 2003)
271. D. Harel, A. Naamad: The STATEMATE Semantics of Statecharts. ACMTransactions on Software Engineering and Methodology (TOSEM) 5, 4 (1996)pp 293-333
272. F. Harrary: Graph Theory (Addison-Wesley, 1972)
273. F. Hausdorff: Set Theory (Oxford University Press, UK 1991)
274. A.E. Haxthausen, X. Yong: Linking DC together with TRSL. In: Proceedingsof 2nd International Conference on Integrated Formal Methods (IFM 2000),Schloss Dagstuhl, Germany, November 2000, no 1945 of Lecture Notes in Computer Science (Springer, 2000) pp 25-44
275. E. Hehner: The Logic of Programming (Prentice Hall, 1984)
276. E. Hehner: A Practical Theory of Programming, 2nd edn (Springer, 1993)
277. A. Hejlsberg, S. Wiltamuth, P. Golde: The C# Programming Language(Addison-Wesley, USA 2003)
278. P. Henderson: Functional Programming: Application and Implementation(Prentice Hall, 1980)
279. J.L. Hennessy, D.A. Patterson: Computer Architecture: a Quantitative Approach (Morgan Kaufmann, 1995)
280. M. Hennessy: Algebraic Theory of Processes (MIT Press, Cambridge, USA,1988)
281. M.C. Henson, S. Reeves, J.P. Bowen: Z Logic and Its Consequences. Computingand Informatics 22, 1-2 (2003)
282. J.R. Hindley: Basic Simple Type Theory (Cambridge University Press, October2002)
283. J.R. Hindley, B. Lercher, J.P. Seldin: Introduction to Combinatory Logic (Cambridge University Press, 1972)
284. J.R. Hindley, J.P. Seldin: Introduction to Combinators and X-Calculus, vol 1of London Mathematical Society, Student Texts (Cambridge University Press,1986)
285. J. Hintikka: Knowledge and Belief: An Introduction to the Logic of the TwoNotions (Cornell University Press, NY, USA 1962)
286. C.A.R. Hoare: Notes on Data Structuring. In: [168] (1972) pp 83-174
287. C.A.R. Hoare: Communicating Sequential Processes. Communications of theACM 21, 8 (1978)
288. C.A.R. Hoare: Communicating Sequential Processes (Prentice Hall, 1985)
289. C.A.R. Hoare. Communicating Sequential Processes. Published electronically:http://www.usingcsp.com/cspbook.pdf, 2004. Second edition of [288]. Seealso http://www.usingcsp.com/.
290. C.A.R. Hoare, et al.: Laws of Programming. Communications of the ACM 30,8 (1987) pp 672-686, 770
291. C.A.R. Hoare, J.F. He: Unifying Theories of Programming (Prentice Hall,1997)
292. C.A.R. Hoare, N. Wirth: An Axiomatic Definition of the Programming Language PASCAL. Acta Informatica 2 (1973) pp 335-355
293. A. Hodges: Alan Turing: the Enigma (Random House, London, UK 1992)
294. W. Hodges: Logic (Penguin Books, 1977)
295. C.J. Hogger: Essentials of Logic Programming (Clarendon Press, 1990)
296. J. Hopcroft, J. Ullman: Introduction to Automata Theory, Languages and Computation (Addison-Wesley, 1979)
297. I. Horebeek, J. Lewi: Algebraic Specifications in Software Engineering. An Introduction (Springer, New York, NY, 1989)
298. W. Humphrey: Managing the Software Process (Addison-Wesley, 1989)
299. IEEE CS. IEEE Standard Glossary of Software Engineering Terminology, 1990.IEEE Std.610.12.
300. D.C. Ince: The Collected Works of A.M. Turing: Mechanical Intelligence(North-Holland, Amsterdam, The Netherlands 1992)
301. Inmos Ltd.: specification of instruction set & Specification of floating pointunit instructions. In: Transputer Instruction Set - A Compiler writer's guide(Prentice Hall, UK 1988) pp 127-161
302. ITU-T. CCITT Recommendation Z.120: Message Sequence Chart (MSC),1992.
303. ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC), 1996.
304. ITU-T. ITU-T Recommendation Z.120: Message Sequence Chart (MSC), 1999.
305. M.A. Jackson: Principles of Program Design (Academic Press, 1969)
306. M.A. Jackson: System Design (Prentice Hall, 1985)
307. M.A. Jackson: Problems, methods and specialisation. Software EngineeringJournal 9, 6 (1994) pp 249-255
308. M.A. Jackson: Software Requirements & Specifications: a lexicon of practice,principles and prejudices (Addison-Wesley, UK 1995)
309. M.A. Jackson: Software Hakubutsushi: sekai to kikai no kijutsu (Software Requirements & Specifications: a lexicon of practice, principles and prejudices)(Toppan Company, Japan 1997)
310. M.A. Jackson: Problem Frames — Analyzing and Structuring Software Development Problems (Addison-Wesley, UK 2001)
311. M.A. Jackson, G. Twaddle: Business Process Implementation — BuildingWorkflow Systems (Addison-Wesley, 1997)
312. J. Jaffar, S. Michaylov: Methodology and Implementation of a CLP System.Technical Report, IBM Research, Yorktown (1987)
313. K. Jensen: Coloured Petri Nets, vol 1: Basic Concepts (234 pages + xii), Vol.2: Analysis Methods (174 pages + x), Vol. 3: Practical Use (265 pages + xi)of EATCS Monographs in Theoretical Computer Science (Springer, Heidelberg1985, revised and corrected second version: 1997)
314. K. Jensen, N. Wirth: Pascal User Manual and Report, vol 18 of LNCS(Springer, 1976)
315. C.B. Jones: Denotational Semantics of GOTO: an Exit Formulation and ItsRelation to Continuations. In: [120] (Springer, 1978) pp 278-304
316. C.B. Jones: Systematic Software Development Using VDM (Prentice Hall,1986)
317. C.B. Jones: Systematic Software Development Using VDM, 2nd edn (PrenticeHall, 1990)
318. C.B. Jones, K. Middelburg: A Typed Logic of Partial Functions ReconstructedClassically. Acta Informatica 31, 5 (1994) pp 399-430
319. N.D. Jones: Computability and Complexity — From a Programming Point ofView (MIT Press, USA, 1996)
320. N.D. Jones, C. Gomard, P. Sestoft: Partial Evaluation and Automatic ProgramGeneration (Prentice Hall, 1993)
321. B. Kernighan, D. Ritchie: C Programming Language, 2nd edn (Prentice Hall,1989)
322. S.C. Kleene: Lambda-definability and recursiveness. Duke Math. J. 2 (1936) pp340-53
323. S.C. Kleene: Introduction to Meta-mathematics (Van Nostrand, New York andToronto, 1952)
324. S.C. Kleene: Mathematical Logic (Dover Publications, 2002)
325. J. Klose, H. Wittke: An Automata Based Interpretation of Live SequenceCharts. In: TACAS 2001, ed by T. Margaria, W. Yi (Springer, 2001) pp 512-527
326. D. Knuth: The Art of Computer Programming, Vol. 1: Fundamental Algorithms(Addison-Wesley, USA, 1968)
327. D. Knuth: The Art of Computer Programming, Vol. 2.: Seminumerical Algorithms (Addison-Wesley, USA, 1969)
328. D. Knuth: The Art of Computer Programming, Vol. 3: Searching & Sorting(Addison-Wesley, USA, 1973)
329. B. Konikowska, A. Tarlecki, A. Blikle: A Three-alued Logic for Software Specification and Validation. In: [135] (1988) pp 218-242
330. I. Lakatos: Proofs and Refutations: The Logic of Mathematical Discovery (Eds.:J. Worrall and E.G. Zahar) (Cambridge University Press, UK 1976)
331. L. Lamport: The Temporal Logic of Actions. ACM Transactions on Programming Languages and Systems 16, 3 (1994) pp 872-923
332. L. Lamport: Specifying Systems (Addison-Wesley, USA 2002)
333. P. Landin: The Mechanical Evaluation of Expressions. Computer Journal 6, 4(1964) pp 308-320
334. P. Landin: A Correspondence Between ALGOL 60 and Church's LambdaNotation (in 2 parts). Communications of the ACM 8, 2-3 (1965) pp 89-101and 158-165
335. P. Landin: A Generalization of Jumps and Labels. Technical Report, UnivacSys. Prgr. Res. Grp., NY (1965)
336. P. Landin: Getting Rid of Labels. Technical Report, Univac Sys. Prgr. Res.Grp., NY (1965)
337. P. Landin: A Formal Description of ALGOL 60. In: [483] (1966) pp 266-294
338. P. Landin: A Lambda Calculus Approach. In: Advances in Programming andNon-numeric Computations, ed by L. Fox (Pergamon Press, 1966) pp 97-141
339. P. Landin: The Next 700 Programming Languages. Communications of theACM 9, 3 (1966) pp 157-166
340. P. Landin. Histories of discoveries of continuations: belles-lettres with equivocaltenses, 1997. In O. Danvy, editor, ACM SIGPLAN Workshop on Continuations,Number NS-96-13 in BRICS Notes Series, 1997.
341. J. Laprie: Dependable computing and fault-tolerance: concepts and terminology. In: 15th. Int. Symp. on Fault-Tolerant Computing (IEEE, 1985)
342. J. Lee: Computer Semantics (Van Nostrand Reinhold, 1972)
343. J. Lee, W. Delmore: The Vienna Definition Language, A Generalization ofInstruction Definitions. In: ACM SIGPLAN Symp. on Programming LanguageDefinitions, San Francisco (1969)
344. Edited by J. van Leeuwen: Handbook of Theoretical Computer Science, VolumesA and B (Elsevier, 1990)
345. H. Leonard, N. Goodman: The Calculus of Individuals and Its Uses. Journalof Symbolic Logic 5 (1940) pp 45-55
346. X. Leroy, P. Weis: Manuel de Reference du langage Caml (InterEditions, Paris,France 1993)
347. S. Levi, A. Agrawala: Real-Time System Design (McGraw-Hill, NY, USA 1990)
348. T. Lindholm, F. Yellin: The Java Virtual Machine Specification (ACM PressBooks, 1996)
349. J. Lipson: Elements of Algebra and Algebraic Computing (Addison-Wesley,USA 1981)
350. W. Little, H. Fowler, J. Coulson, C. Onions: The Shorter Oxford English Dictionary on Historical Principles (Clarendon Press, UK, 1987)
351. J. Lloyd: Foundation of Logic Programming (Springer, 1984)
352. H.H. L0vengreen, D. Bj0rner: On a Formal Model of the Tasking Concepts inAda. In: ACM SIGPLAN Ada Symp. (1980)
353. P. Lucas: Formal Semantics of Programming Languages: VDL. IBM Journalof Devt. and Res. 25, 5 (1981) pp 549-561
354. P. Lucas, K. Walk: On the Formal Description of PL/I. Annual Review Automatic Programming Part 3 6, 3 (1969)
355. E. Luschei: The Logical Systems of Lesniewski (North-Holland, Amsterdam,The Netherlands 1962)
356. J. Liitzen: Joseph Liouville 1809-1882: Master of Pure and Applied Mathematics, vol 15 of Studies in the History of Mathematics and Physical Sciences(Springer, New York - Berlin 1990)
357. N. Lynch: Distributed Algorithms (Morgan Kaufmann Publishers, 1996)
358. C. MacPherson: Burke (Oxford University Press, 1980)
359. Z. Manna: Mathematical Theory of Computation (McGraw-Hill, 1974)
360. Z. Manna, A. Pnueli: The Temporal Logic of Reactive Systems: Specifications(Addison-Wesley, 1991)
361. Z. Manna, A. Pnueli: The Temporal Logic of Reactive Systems: Safety(Addison-Wesley, 1995)
362. Z. Manna, R. Waldinger: The Logical Basis for Computer Programming,Vols. 1-2 (Addison-Wesley, 1985-90)
363. W. Mao: Modern Cryptography: Theory and Practice (Pearson ProfessionalEducation, Prentice Hall, 2003)
364. D. May: occam (Prentice Hall, UK 1982)
365. J. McCarthy: Recursive Functions of Symbolic Expressions and Their Computation by Machines, Part I. Communications of the ACM 3, 4 (1960) pp184-195
366. J. McCarthy: Towards a Mathematical Science of Computation. In: IFIP WorldCongress Proceedings, ed by C. Popplewell (1962) pp 21-28
367. J. McCarthy: A Basis for a Mathematical Theory of Computation. In: Computer Programming and Formal Systems (North-Holland, Amsterdam, 1963)
368. J. McCarthy: A Formal Description of a Subset of ALGOL. In: [483] (1966)
369. J. McCarthy. Artificial Intellingence. Electronically, on the Web: h t t p : / / -www-formal.Stanford.edu/jmc/, 2004.
370. J. McCarthy, et al.: LISP 1.5, Programmer's Manual (The MIT Press, USA1962)
371. K. Mehlhorn: Data Structures and Algorithms: 3 vols.: 1: Multi-dimensionalSearching and Computational Geometry, 2: Graph Algorithms and NPCompleteness, 3: Sorting and Searching (Springer, 1984)
372. E. Mendelsohn: Introduction to Mathematical Logic, 4th edn (Lewis Publishers,International Thomson Publishing, June 1, 1997)
373. Merriam-Webster. Online Dictionary: http://www.m-w.com/home.htm, 2004.Merriam-Webster, USA.
374. J. Meseguer: Software Specification and Verification in Rewriting Logic. NATOAdvanced Study Institute (2003)
375. B. Meyer: On Formalism in Specifications. IEEE Software 2, 1 (1985) pp 6-26
376. B. Meyer: Object-oriented Software Construction (Prentice Hall, 1988)
377. B. Meyer: Eiffel: The Language, second revised edn (Prentice Hall, USA 1992)
378. B. Meyer: Object-oriented Software Construction, second revised edn (PrenticeHall, USA 1997)
379. J. Meyer, T. Downing, A. Shulmann: Java Virtual Machine (O'Reilly h Associates, 1997)
380. G. Michaelson: Introduction to Functional Programming Through LambdaCalculus (Addison-Wesley, 1989)
381. Microsoft Corporation: MCAD/MCSD Self-Paced Training Kit: DevelopingWeb Applications with Microsoft Visual Basic .NET and Microsoft Visual C#.NET (Microsoft Corporation, Redmond, WA, USA 2002)
382. Microsoft Corporation: MCAD/MCSD Self-Paced Training Kit: DevelopingWindows-Based Applications with Microsoft Visual Basic .NET and MicrosoftVisual C# .NET (Microsoft Corporation, Redmond, WA, USA 2002)
383. D. Mieville, D. Vernant: Stanislaw Lesniewski aujourd'hui Grenoble, October8-10, 1992 (Neuchatel, 1996)
384. P. Millican, A. Clark: The Legacy of Alan Turing: Machines and Thought (Oxford University Press, UK 1999)
385. R. Milne, C. Strachey: A Theory of Programming Language Semantics (Chapman and Hall, London, Halsted Press/Wiley, NY 1976)
386. R. Milner: Calculus of Communication Systems, vol 94 of Lecture Notes inComputer Science (Springer, 1980)
387. R. Milner: Communication and Concurrency (Prentice Hall, 1989)
388. R. Milner: Communicating and Mobile Systems: The ^-Calculus (CambridgeUniversity Press, 1999)
389. R. Milner, M. Tofte, R. Harper: The Definition of Standard ML (MIT Press,USA and UK, 1990)
390. C.C. Morgan: Programming from Specifications (Prentice Hall, UK 1990)
391. J. Morris: Lambda-Calculus Models of Programming Languages. PhD Thesis,Lab. for Computer Science, Mass. Inst, of Techn., Cambridge, USA, TR-57(1968)
392. L. Morris: The Next 700 Programming Language Descriptions. Unpubl. ms.,Univ. of Essex, Comp. Ctr. (1970)
393. L. Morris: Advice on Structuring Compilers and Proving Them Correct. In:Principles of Programming Languages, SIGPLAN/SIGACT Symposium, ACMConference Record/Proceedings (1973) pp 144-152
394. Y.N. Moschovakis: Notes on Set Theory (Springer, Heidelberg, 1994)
395. T. Mossakowski, A.E. Haxthausen, D. Sanella, A. Tarlecki: CASL — The Common Algebraic Specification Language: Semantics and Proof Theory. Computing and Informatics 22, 1-2 (2003)
396. P.D. Mosses: Action Semantics (Cambridge University Press, 1992)
397. P.D. Mosses: CoFI: The Common Framework Initiative for Algebraic Specification. Bull. EATCS 59 (1996) pp 127-132
398. P.D. Mosses: CASL for CafeOBJ users. In: CAFE: An Industrial-Strength Algebraic Formal Method (Elsevier, 2000) pp 121-144
399. Edited by P.D. Mosses: CASL Reference Manual, vol 2960 of LNCS (Springer,Heidelberg 2004)
400. B.C. Moszkowski: Executing Temporal Logic Programs (Cambridge UniversityPress, UK 1986)
401. Edited by G. Nelson: Systems Programming in Modula 3 (Prentice Hall, USA1991)
402. A. Nerode, R. Shore: Logic for Applications (Springer, 1997)
403. D.E. Newton: Alan Turing (Xlibris Corporation, 2003)
404. J.F. Nilsson: Formal Vienna Development Method Models of PROLOG. In:Implementations of PROLOG, ed by J. Campbell (Ellis Horwood Series: Artificial Intelligence, 1984) pp 281-308
405. J.F. Nilsson. Some Foundational Issues in Ontological Engineering, October30 - Novewmber 1 2002. Lecture slides for a PhD Course in RepresentationFormalisms for Ontologies, Techn. Univ. of Denmark.
406. T. Nipkow, L.C. Paulson, M. Wenzel: Isabelle/HOL, A Proof Assistant forHigher-Order Logic, vol 2283 of LNCS (Springer, Heidelberg, Germany, 2002)
407. B. Nordstrom, K. Petersson, J.M. Smith: Programming in Martin-Lof's TypeTheory An Introduction, vol 7 of International Series of Monographs on Computer Science (Clarendon Press, Oxford University Press, UK 1990) p 232
408. Object Management Group: OMG Unified Modelling Language Specification,version 1.5 edn (OMG/UML, http://www .omg.org/uml/ 2003)
409. O. Ore: Graphs and Their Uses (The Mathematical Association of America,1963)
410. S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert. PVS LanguageReference. Computer Science Laboratory, SRI International, CA, 1999.
411. S. Owre, N. Shankar, J.M. Rushby, D.W.J. Stringer-Calvert. PVS SystemGuide. Computer Science Laboratory, SRI International, Menlo Park, CA,Sept. 1999.
412. Oxford University Press: The Oxford Dictionary of Quotations (Oxford University Press, UK 1974)
413. D.L. Parnas: On the criteria to be used in Decomposing Systems into Modules.Communications of the ACM 15, 12 (1972) pp 1053-1058
414. D.L. Parnas: A technique for Software Module Specification with Examples.Communications of the ACM 14, 5 (1972)
415. D.L. Parnas: Software Fundamentals: Collected Papers, Eds.: David M. Weissand Daniel M. Hoffmann (Addison-Wesley, 2001)
416. D.L. Parnas, P.C. Clements: A Rational Design Process: How and Why to Fakeit. IEEE Trans. Software Engineering 12, 2 (1986) pp 251-257
417. D.L. Parnas, P.C. Clements, D.M. Weiss: Enhancing reusability with information hiding. In: Tutorial: Software Reusability (Ed.: Peter Freeman) (IEEEPress, 1986) pp 83-90
418. D.A. Patterson, J.L. Hennessy: Computer Organization and Design (MorganKaufmann, 1998)
419. L. Paulson: Isabelle: The Next 700 Theorem Provers. In: Logic in ComputerScience, ed by P. Oddifreddi (Academic Press, 1990) pp 361-386
420. R. Penner: Discrete Mathematics, Proof Techniques and Mathematical Structures (World Scientific, Singapore 1999)
421. CA . Petri: Kommunikation mit Automaten (Bonn: Institut fur InstrumentelleMathematik, Schriften des IIM Nr. 2, 1962)
422. C. Petzold: Programming Windows with C# (Core Reference) (Microsoft Corporation, Redmond, WA, USA 2001)
423. S.L. Pfleeger: Software Engineering, Theory and Practice, 2nd edn (PrenticeHall, 2001)
424. B. Pierce: Types and Programming Languages (MIT Press, 2002)
425. M. Piff: Discrete Mathematics, An Introduction for Software Engineers (Cambridge University Press, UK 1991)
426. G.D. Plotkin: Call-by-Name, Call-by-Value and the Lambda Calculus. Theoretical Computer Science 1 (1975) pp 125-159
427. G.D. Plotkin: A Structural Approach to Operational Semantics. Technical Report, Comp. Sci. Dept., Aarhus Univ., Denmark; DAIMI-FN-19 (1981)
428. G.D. Plotkin: A Structural Approach Operational Semantics. Journal of Logicand Algebraic Programming 60-61 (2004) pp 17-139
429. A. Pnueli: The Temporal Logic of Programs. In: Proceedings of the 18th IEEESymposium on Foundations of Computer Science (IEEE CS, 1977) pp 46-57
430. R.S. Pressman: Software Engineering, A Practitioner's Approach, 5th edn(McGraw-Hill, 1981-2001)
431. M. Penicka, A.K. Strupchanska, D. Bj0rner: Train Maintenance Routing. In:FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems (L'Harmattan Hongrie, 2003)
432. B. Randell: On Failures and Faults. In: FME 2003: Formal Methods, vol 2805of Lecture Notes in Computer Science (Springer, 2003) pp 18-39
433. C. Reade: Elements of Functional Programming (Addison-Wesley, 1989)
434. M. Reiser: The 0BER0N System, User Guide and Programmer's Manual(Addison-Wesley, 1991)
435. W. Reisig: Petri Nets: An Introduction, vol 4 of EATCS Monographs in Theoretical Computer Science (Springer, 1985)
436. W. Reisig: A Primer in Petri Net Design (Springer, 1992)
437. W. Reisig: Elements of Distributed Algorithms: Modelling and Analysis withPetri Nets (Springer, 1998)
438. W. Reisig: On Gurevich's Theorem for Sequential Algorithms. Acta Informatica(2003)
439. W. Reisig: The Expressive Power of Abstract-State Machines. Computing andInformatics 22, 1-2 (2003)
440. J.C. Reynolds: On the Relation Between Direct and Continuation Semantics.In: International Colloquium on Automata, Languages and Programming, European Association for Theoretical Computer Science (Springer, 1974) pp 157-168
441. J.C. Reynolds: The Craft of Programming (Prentice Hall, 1981)
442. J.C. Reynolds: Theories of Programming Languages (Cambridge UniversityPress, UK 1998)
443. J.C. Reynolds: The Semantics of Programming Languages (Cambridge University Press, UK 1999)
444. H.R. Rogers: Theory of Recursive Functions and Effective Computability(McGraw-Hill, 1967)
445. P. Roget: Rogers Thesaurus (Collins, London and Glasgow, 1974)
446. Edited by A.W. Roscoe: A Classical Mind: Essays in Honour of C.A.R. Hoare(Prentice Hall, 1994)
447. A.W. Roscoe. Model Checking CSP, pages 353-378. Prentice Hall, 1994
448. A.W. Roscoe: Theory and Practice of Concurrency (Prentice Hall, 1997)
449. A.W. Roscoe, C.A.R. Hoare: Laws of occam Programming. Theoretical Computer Science 60 (1988) pp 177-229
450. Edited by A.W. Roscoe, J.C.P. Woodcock: A Millennium Perspective on Informatics (Palgrave, 2001)
451. J. Rushby: Formal Methods and the Certification of Critical Systems. TechnicalReport SRI-CSL-93-7, Computer Science Laboratory, SRI International, MenloPark, CA., USA (1993)
452. J. Rushby: Formal Methods and Their Role in the Certification of CriticalSystems. Technical Report SRI-CSL-95-1, Computer Science Laboratory, SRIInternational, Menlo Park, CA (1995)
453. D. Sangiorgio, D. Walker: The ^-Calculus (Cambridge University Press, 2001)
454. D.A. Schmidt: Denotational Semantics: a Methodology for Language Development (Allyn & Bacon, 1986)
455. D.A. Schmidt: The Structure of Typed Programming Languages (MIT Press,1994)
456. S. Schneider: Concurrent and Real-Time Systems — The CSP Approach (Wiley, UK 2000)
457. J.R. Schoenfeld: Mathematical Logic (A.K. Peters, 2001)
458. D. Scott: The Lattice of Flow Diagrams. In: [212] (1970) pp 311-366
459. D. Scott: Outline of a Mathematical Theory of Computation. In: Proc. J^thAnn. Princeton Conf. on Inf. Sci. and Sys. (1970) p 169
460. D. Scott: Continuous Lattices. In: Toposes, Algebraic Geometry and Logic, edby F. Lawvere (Springer, Lecture Notes in Mathematics, Vol. 274 1972) pp97-136
461. D. Scott: Data Types as Lattices. Unpublished Lecture Notes, Amsterdam(1972)
462. D. Scott: Lattice Theory, Data Types and Semantics. In: Symp. Formal Semantics, pp 67-106, ed by R. Rustin (Prentice Hall, 1972)
463. D. Scott: Mathematical Concepts in Programming Language Semantics. In:Proc. AFIPS, Spring Joint Computer Conference, 40 (1972) pp 225-234
464. D. Scott: Lattice-Theoretic Models for Various Type Free Calculi. In: Proc. 4thIntl. Congr. for Logic Methodology and the Philosophy of Science, Bucharest(North-Holland, Amsterdam, 1973) pp 157-187
465. D. Scott: A-Calculus and Computer Science Theory. In: Lecture Notes in Computer Science, Vol. 37, ed by C. Bohm (Springer, 1975)
466. D. Scott: Data Types as Lattices. SIAM Journal on Computer Science 5, 3(1976) pp 522-587
467. D. Scott: Domains for Denotational Semantics. In: International Colloquium onAutomata, Languages and Programming, European Association for TheoreticalComputer Science (Springer, 1982) pp 577-613
468. D. Scott: Some Ordered Sets in Computer Science. In: Ordered Sets, ed by I.Rival (Reidel Publ., 1982) pp 677-718
469. D. Scott, C. Strachey: Towards a Mathematical Semantics for Computer Languages. In: Computers and Automata, vol 21 of Microwave Research Inst. Symposia (1971) pp 19-46
470. P. Sestoft: Java Precisely (MIT Press, 2002)
471. R. Sethi, A. Tang: Constructing Call-by-Value Continuation Semantics. Journal of the ACM 27 (1980) pp 580-597
472. N. Shankar: Metamathematics, Machines and G'odeVs Proof (Cambridge University Press, UK 1994)
473. P.M. Simons. LesniewskVs Logic and Its Relation to Classical and Free Logics.In: Foundations of Logic and Linguistics: Problems and Their Solutions, GeorgDorn and P. Weingartner (Eds.). Plenum Press, NY, 1985.
474. S. Sokolowski: Applicative Higher-Order Programming: the Standard ML Perspective (Chapman and Hall, 1991)
475. I. Sommerville: Software Engineering, 6th edn (Addison-Wesley, 1982-2001)
476. J.M. Spivey: Understanding Z: A Specification Language and Its Formal Semantics, vol 3 of Cambridge Tracts in Theoretical Computer Science (Cambridge University Press, 1988)
477. J.M. Spivey: The Z Notation: A Reference Manual (Prentice Hall, UK 1989)
478. J.M. Spivey: The Z Notation: A Reference Manual, 2nd edn (Prentice Hall,1992)
479. Edited by J.T.J. Srzednicki, Z. Stachniak: LesniewskVs lecture notes in logic(Dordrecht, 1988)
480. J.T.J. Srzednicki, Z. Stachniak: Lesniewski's systems protothetic (Dordrecht,1998)
481. D.F. Stanat, D.F. McAllister: Discrete Mathematics for Computer Science(Prentice Hall, 1977)
482. Edited by J. Staunstrup, W. Wolff: Hardware/Software Co-design: Principlesand Practice (Kluwer Academic Press, The Netherlands 1997)
483. Edited by T.B. Steel: Formal Language Description Languages, IFIP TC-2Work. Conf., Baden (North-Holland, Amsterdam, 1966)
484. Edited by J. Stein: The Random House American Everyday Dictionary (Random House, NY, USA 1949, 1961)
485. C. Strachey: Fundamental Concepts in Programming Languages. Unpubl. Lecture Notes, NATO Summer School, Copenhagen, 1967, and Programming Research Group, Oxford Univ. (1968)
486. C. Strachey: The Varieties of Programming Languages. Techn. Monograph 10,Programming Research Group, Oxford Univ. (1973)
487. C. Strachey: Continuations: A Mathematical Semantics which can deal withFull Jumps. Techn. Monograph, Programming Research Group, Oxford Univ.(1974)
488. H. Strong: Translating Recursion Equations into Flow Charts. In: Proceedings2nd Annual ACM Symposium on Theory of Computig (SToC) (1970) pp 184-197
489. B. Stroustrup: C+ + Programming Language (Addison-Wesley, 1986)
490. A.K. Strupchanska, M. Penicka, D. Bj0rner: Railway Staff Rostering. In:FORMS 2003: Symposium on Formal Methods for Railway Operation and Control Systems (L'Harmattan Hongrie, 2003)
491. P.R. Suppes: Axiomatic Set Theory (Dover, NY, USA 7 May 1973)
492. P.R. Suppes, S. Hill: A First Course in Mathematical Logic (Dover, July 1,2002)
493. Edited by S.J. Surma, J.T. Srzednicki, D.I. Barnett, V.F. Rickey: StanislawLesniewski: Collected Works (2 Vols.) (Dordrecht, Boston - New York 1988)
494. V.G. Szebehely: Adventures in Celestial Mechanics. A First Course in the Theory of Orbits (University of Texas Press, USA 1993)
495. R. Tarjan: Data Structures and Network Algorithms (SIAM: Soc. for Ind. &Appl. Math., 1983)
496. R. Tennent: Principles of Programming Languages (Prentice Hall, 1981)
497. R. Tennent: The Semantics of Programming Languages (Prentice Hall, 1997)
498. S. Thompson: Haskell: The Craft of Functional Programming, 2nd edn(Addison-Wesley, 1999)
499. F.X. Tong: From the Soil — The Foundations of Chinese Society: XiangTuZhongGuo (University of California Press, USA (1947) 1992)
500. G. Tourlakis: Lectures in Logic and Set Theory: Volume 2, Set Theory (Cambridge University Press, UK 2003)
501. W.A. Triebel: The 80386, 80486, and Pentium Microprocessors (Prentice Hall,1998)
502. D. Turner: Miranda: A Non-strict Functional Language with PolymorphicTypes. In: Functional Programming Languages and Computer Architectures,no 201 of Lecture Notes in Computer Science, ed by J. Jouannaud (Springer,Heidelberg, Germany, 1985)
503. J. van Benthem: The Logic of Time, vol 156 of Synthese Library: Studies inEpistemology, Logic, Methhodology, and Philosophy of Science (Editor: JaakkoHintika), 2nd edn (Kluwer Academic, The Netherlands 1991)
504. R. van Glabbeek, P. Weijland. Branching Time and Abstraction in Bisimulation Semantics. Electronically, on the Web: h t t p : / / t h e o r y . S t a n f o r d . -edu/~rvg/abstraction/abstraction.html, Centrum voor Wiskunde en Informatica, Postbus 94079, 1090 GB Amsterdam, The Netherlands, January1996.
505. W. van Orman Quine: Set Theory and Its Logic (Harvard University Press,USA 1969)
506. W. van Orman Quine: From a Logical Point of View (Harvard Univ. Press,USA 1980)
507. W. van Orman Quine: Word and Object (MIT Press, USA 1960)
508. W. van Orman Quine: Pursuit of Truth, paperback edn (Harvard Univ. Press,USA 1992)
509. W. van Orman Quine: Mathematical Logic (Harvard University Press, 1979)
510. A. van Wijngaarden: Report on the Algorithmic Language ALGOL 68. ActaInformatica 5 (1975) pp 1-236
511. B. Venners: Inside the Java 2.0 Virtual Machine (Enterprise Computing)(McGraw-Hill, 1999)
512. H. van Vliet: Software Engineering: Principles and Practice (Wiley, UK 2000)
513. C. Wadsworth: Semantics and Pragmatics of the Lambda-Calculus. PhD Thesis, Programming Research Group, Oxford Univ., (1971)
514. M. Wand: Continuation-Based Program Transformation Strategies. Journal ofthe ACM 27 (1980) pp 164-180
515. M. Wand: Induction, Recursion and Programming (North-Holland, Amsterdam, 1980)
516. D. Watt, B. Wichmann, W. Findlay: Ada: Language and Methodology (PrenticeHall, 1986)
517. P. Wegner: Programming Languages, Information Structures, and Machine Organization (McGraw-Hill, 1968)
518. P. Weis, X. Leroy: Le langage Caml (Dunod, Paris, France 1999)
519. Wikipedia: Polymorphism. In: Internet (Published: http://en.wikipedia.org/-wiki/Polymorphism_(computer.science), 2005)
520. A. Wikstrom: Functional Programming Using Standard ML (Prentice Hall,1984)
521. G. Winskel: The Formal Semantics of Programming Languages (The MITPress, USA, 1993)
522. N. Wirth: The Programming Language PASCAL. Acta Informatica 1, 1 (1971)pp 35-63
523. N. Wirth: Systematic Programming (Prentice Hall, 1973)
524. N. Wirth: Algorithms + Data Structures = Programs (Prentice Hall, 1976)
525. N. Wirth: Programming in Modula-2 (Springer, Heidelberg, 1982)
526. N. Wirth: From Modula to Oberon. Software — Practice and Experience 18(1988) pp 661-670
527. N. Wirth: The Programming Language Oberon. Software — Practice and Experience 18 (1988) pp 671-690
528. N. Wirth: The Programming Language Oberon. Software — Practice and Experience 18 (1988) pp 671-690
529. N. Wirth, J. Gutknecht: The Oberon System. Software — Practice and Experience 19, 9 (1989) pp 857-893
530. N. Wirth, J. Gutknecht: The Oberon Project (Addison-Wesley, 1992)
531. N. Wirth, C.A.R. Hoare: A Contribution to the Development of ALGOL. Communications of the ACM 9, 6 (1966) pp 413-432
532. D.A. Wolfram: The Clausal Theory of Types (Cambridge University Press,March 1993)
533. J.C.P. Woodcock, J. Davies: Using Z: Specification, Proof and Refinement(Prentice Hall, 1996)
534. J.C.P. Woodcock, M. Loomes: Software Engineering Mathematics (Pitman,London, 1988)
535. Y. Xia, C.W. George: An Operational Semantics for Timed RAISE. In: FM'99— Formal Methods, ed by J.M. Wing, J. Woodcock, J. Davies (Springer, 1999)pp 1008-1027
536. E.N. Zalta: Logic. In: The Stanford Encyclopedia of Philosophy (Published:http://plato.stanford.edu/, Winter 2003)
537. C.C. Zhou, M.R. Hansen: Duration Calculus: A Formal Approach to Real-Time Systems (Springer, 2004)
538. C.C. Zhou, C.A.R. Hoare, A.P. Ravn: A Calculus of Durations. Information Proc. Letters 40, 5 (1992)