高级搜索 书名 作者 ISBN

软件工程卷2：系统与语言规约

图书分类   计算机考试类图书   计算机等级考试 软件资格水平考试 计算机类认证考试 数学   基础数学教材 数学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 物理   基础物理教材 物理专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 力学   基础力学教材 力学专业及研究生教材 教辅及考研图书 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 化学化工   基础化学 化学 化工 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 机械材料汽车能源   机械 仪器仪表 材料 汽车 能源与动力工程 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 工业工程   国外大学优秀教材-工业工程系列(影印版) 国外大学优秀教材-工业工程系列(翻译版) 物流供应链丛书 其他 普通高等学校物流管理专业系列教材 工业设计   工业设计 建筑土木水利   建筑学（教材） 建筑设计及建筑文化 土木工程 水利工程 工程管理 环境与给排水   环境科学与环境工程 给排水 引进图书 专著、工具书及其他参考书 多媒体课件及网络教学资源 生物与医学   医学与生物学教材 教学辅导及考试用书 引进版图书 专业工具书和手册 医学专业参考书 生物学专业参考书 大众读物 电工基础与电气工程   电工基础 电气工程 专著、工具书及其他参考书 多媒体课件及网络教学资源 科普读物   院士科普第一辑 院士科普第二辑 院士科普第三辑 院士科普第四辑 走进科学殿堂 华裔科学家科普文集 其他 辞书   辞书 社会职业培训   工程技术操作技能类 城市服务业基础技能类 就业素质教育类 其他 航空航天   航空航天 计算机基础   计算机文化基础 办公自动化 应用基础 公共基础 软件技术基础 计算机导论 计算机组成与原理   计算机组成 计算机原理 接口技术 操作系统 算法与程序设计   C程序设计 数据结构 C++语言 编译原理 Visual Basic Java 汇编语言 FoxPro Delphi 算法 pb 计算机技术及应用   计算机技术及应用 计算机网络   Internet TCP/IP 计算机网络 网页制作 电子商务 网络安全 图形图像与多媒体   图形学 多媒体 图形图像 计算机辅助设计   计算机辅助设计 AutoCAD CATIA 数据库   SQL Server FoxPro Access Oracle 数据库原理 数据挖掘 PowerBuilder 软件工程   软件工程导论 软件工程 数理基础   数字逻辑 离散数学 线性代数 数理基础 信息安全   密码学 概论 病毒防护 电子信息   电子信息基础 通信工程 微电子 光电子 自动化 电子信息与计算机 计算机--其他   其他 经济管理   人力资源管理 物流 工商管理 市场营销 经济学 经济读物 金融学 财政学 国际经济贸易 会计学 旅游管理 公共管理 电子商务 考试用书 其他 管理科学与工程 人文社科   伦理学 教育学 心理学 哲学 语言文学 史学 新闻传播学 体育 其他 政治学 社会学 清华校史读物 综合 法律   司法考试用书 法律知识读物 宪法与行政法 法理法史 刑法 诉讼法 经济法 民商法 国际法 知识产权法 司法案例 比较法 艺术   服装艺术设计 工业设计 环境艺术设计 建筑 染织艺术设计 摄影艺术设计 视觉传达艺术设计 书法 陶瓷艺术设计 信息艺术与设计 绘画 雕塑 工艺美术 艺术设计学 艺术类基础教学 非英语专业本科教材   非英语专业本科教材 非英语专业研究生教材   非英语专业研究生教材 专升本教材   专升本教材 英语专业教材   英语专业教材 选修课系列教材   选修课系列教材 专门用途英语教材   商务英语 其他 学术类图书   学术类图书 考试类用书   国内考试用书 国外考试用书 工具书   工具书 娱乐休闲英语   娱乐休闲英语 英语学习方法   英语学习方法 非英语语种图书   日语 德语 外语--其他   其他 高职高专--公共基础课   公共基础课系列 高职高专--人文社科类   法律专业 新闻 高职高专--计算机类   计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 电子商务专业 嵌入式设计 高职高专--电子信息类   电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 高职高专--机电类   机电一体化专业 汽车专业 机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 高职高专--工科类   建筑专业 工程管理专业 高职高专--经济管理类   经济管理基础系列 市场营销专业 财务会计专业 企业管理专业 物流管理专业 财政金融专业 电子商务专业 国际商务专业 人力资源管理专业 高职高专--服务类   旅游专业 饭店管理专业 文秘专业 艺术设计专业 物业管理专业 基础教育--英语   教材教辅 课外读物 综合知识 基础教育--信息技术   教材教参 课外读物 教师培训 科普读物 中职教育--计算机类   计算机基础教育系列 计算机专业基础系列 计算机应用专业 网络专业 软件专业 数据库专业 多媒体技术专业 中职教育--公共课   公共基础课系列 中职教育--经济管理类   经济管理基础类 物流管理专业 财政金融专业 市场营销专业 企业管理专业 国际商务专业 财务会计专业 中职教育--电子信息类   电子信息基础系列 微电子技术专业 通信技术专业 电气自动化专业 应用电子技术专业 中职教育--机电类   机械基础系列 机械设计与制造专业 数控技术专业 模具设计与制造专业 机电一体化专业 汽车专业 中职教育--服务类   旅游专业 饭店管理专业 文秘专业 艺术设计专业 软件工程卷2：系统与语言规约 作者：Dines Bjorner著刘伯超等 图书详细信息： ISBN：9787302208914 定价：79元 印次：1-1 装帧：平装 印刷日期：2009-12-8 图书简介： 本书是世界著名的计算机科学家Dines Bjorner教授对其所从事的软件工程研究 的总结。 这几卷书主要讲述了如何使用形式方法指导软件工程的开发，特别是作者独创性 地提出了领域工程这一全新的研究领域并在第~3~卷中予以系统的论述。作者结合~ RAISE（工业软件开发的严格方法）规约语言，详细阐释了在软件的领域分析、 需求分析、软件设计和开发的各个阶段，如何采用形式方法来指导软件开发模式， 来保证软件开发的可靠性和正确性。 前言： 023237-01.txt 译者序 本书是世界著名的计算机科学家Dines Bjorner教授对其所从事的软件工程研究 的总结。 这几卷书主要讲述了如何使用形式方法指导软件工程的开发，特别是作者独创性 地提出了领域工程这一全新的研究领域并在第3卷中予以系统的论述。作者结合 RAISE（工业软件开发的严格方法）规约语言，详细阐释了在软件的领域分析、 需求分析、软件设计和开发的各个阶段，如何采用形式方法来指导软件开发模式， 来保证软件开发的可靠性和正确性。 在翻译的过程中，译者得到了Dines Bj\orner教授的大力支持。他非常关心中 国学者在软件工程这一领域的研究，热心推动我们将他的三卷著作介绍给中国读 者。 向剑文翻译了前言和第1-3章，刘伯超翻译了第4-13章、第16-20章以及附 录A，孔维强翻译了第14-15章。参加翻译和校对工作的还有田璟、王明华、袁春阳、李智伟、周琼琼、 楚国华、齐亮、司慧勇、陈永然、李佳。限于译者水平，译文中难免会出现一些错误和 不妥之处，敬请读者和专家予以批评指正。 序言 本卷是有关软件工程的工程原则与技术的三卷书中的第2卷。有关本丛书这几卷的一个适当的序言及总体介绍，请参阅第1卷的序言 及该卷的第1章。我们假设读者已经学习了第1卷。 概述 本卷集中讨论对语言和系统进行规约的原则与技术。 它使用在第1卷中 介绍的抽象与建模原则、技术和工具，并且进一步补充了那些原则、技术和工具。 本卷特别强调以下四个方面： 高级规约刻面： 层次和复合 第\ref2ch2章 指称和计算 第\ref2ch3章 格局：上下文和状态 第\ref2ch4章 时间、空间和空间/时间 第\ref2ch5章 模块化 第\ref2ch10章 自动机和机器 第\ref2ch11章 语言学： 语用 第\ref2ch6章 语义 第\ref2ch7章 句法 第\ref2ch8章 符号体系 第\ref2ch9章 并发与时态： 佩特里网 第\ref2ch12章 消息序列图与活序列图 第\ref2ch13章 状态图 第\ref2ch14章 时间的定量模型 第\ref2ch15章 解释器与编译器定义： SAL：简单应用式语言 第\ref2ch16章 SIL：简单命令式语言 第\ref2ch17章 SMIL：简单模块命令式语言 第\ref2ch18章 SPIL：简单并行命令式语言 第\ref2ch19章 “UML”化的形式技术 在这里需要强调一些值得注意的特点。 在并发方面，第\ref2ch12-14章，也举例说明了图解的规约， 正如第\ref2ch9.uml节（\textttUML类图）所作的那样。该材料同时举例说明 了可以简单并娴雅地包含（即通过\dbrsl来使用）统一建模语言（\textttUML \citeuml）的流行特点。 Christian Krog Madsen是第\ref2ch12-\ref2ch14章的主要作者。 \textttRAISE规约语言： 与第1卷一样，在本卷中我们大量使用\dbrsl。因此我们在第\ref2ch1章中插入 一段\dbrsl的入门材料------其他的材料请参阅\textttRAISE的链接地址： \texttthttp://\ www.iist.unu.edu/raise/。 致谢 第1卷的序言包含了一个详尽的致谢章节。 \dbrsl与佩特里网（第\ref2ch12章）、\indexcind佩特里网 消息序列图\indexcindMSC!消息序列图或活序列图\indexcindLSC!活序 列图（第13章）以及状态图（第14章）\indexcind状态图 的结合主要归功于Christian Krog Madsen \citeckm1,ckm2。 \indexaindKrog Madsen, Christian \citeckm1,ckm2% 在此向Christian致以大量及真诚的感谢。\dbrsl与类似 \textttUML的\indexcindUML类图（第\ref2ch9.uml节）的结合主要 归功于Steffen Holmslykke\aindexholmslykke\ \cite2s1,2s2。 同样的感谢亲切地致给Steffen。 Martin P\veni\vcka \indexaindP\veni\vcka, Martin \citeMartinPenicka% 提供了例\ref2ch1-ptpn.railway （第\ref2ch11-ptpn.4节）、 例\ref2ch13-sc-ex.1 （第\ref2ch13.exs.1节）和例 \ref2ch13-sc-ex.2 （第\ref2ch13.exs.2节），在此同样真诚地致以感谢。 新加坡国立大学的同事Andrei Stefan和Yang ShaoFa研究并校对了 第\ref2ch12-\ref2ch15章。同作为主要人物的Yang ShaoFa一起 \indexaindYang Shaofa，我决定设计了第\ref2ch13.ctp节中的 CTP\indexcindCTP!通信事务进程 （Communicating Transaction Processes，通信事务进程）模型。十分感谢他们的意见及工作。 从1976年至今在丹麦技术大学的30年经历是我在学术上快乐的一个主要源泉。 最后但并非最不重要的，我对施普林格的编辑Ronan Nugent的巨大支持表示感谢。 第2卷的简要指南 这一卷有若干章节。这些章节被归类成几个部分。图2概括了 一个这些章节中的优先关系。该图把学习该卷的建议顺序放在一起。 第1章被认为是学习任何章节的一个先决条件。 我们把一些部分分组成虚线环绕的组$A-E$。 组$A$由第2-5章所组成，可以以任何顺序进行学习。 组$B$由第6-9章所组成，应该按照6、7、8和9的顺序进行学习。 组$C$由第10-11章所组成，可以以任何顺序进行学习。 组$D$由第12-15章所组成，可以以任何顺序进行学习。 第14章包含一个需要首先学习第13章的例子。 组$E$由第16-19章所组成， 应该按照16、17和18的顺序 进行学习。第19章可以在中间、之前或之后进行学习。最好在之后。 组$A\sim E$可以以任意顺序进行学习。但是在第15章之前先学习 第5章，在第18章之前先学习第10章，以及在组$E$之前先 学习组$B$可能会有帮助。 学习第20章是没有害处的。 附录A包含一个我们的命名约定的综述。 \noindent 在大多数章中有许多小节可以被略过。典型地是那些带有较大的例子或接近于 章的结尾部分的小节。 教师或读者可以用这种方式组合成许多适当的课程。在图1中建议了一些 这样的课程。 图1\quad 仅基于第2卷的可供选择的课程 Dines Bj\orner \textsl丹麦技术大学，2005--2006 图2\quad 章节优先次序图 目录： 023237-01.txt 原著作者为中文版所作的序 译者序 序言ix 概述ix “UML”化的形式技术x RAISE 规约语言： RSLx 致谢x 第 2 卷的简要指南xi part I 开篇1 xpart开篇1 chapter 1序言3 1.1前言3 1.1.1为什么有本卷3 1.1.2为什么要掌握这些原理、技术与工具3 1.1.3本卷“包含”了什么4 1.1.4本卷是如何“陈述”的5 1.2“轻量级”形式技术5 1.3 RSL 的入门读物7 1.3.1类型7 类型表达式7 类型定义8 具体类型8 子类型9 分类 ------ 抽象类型9 1.3.2 RSL 谓词演算10 命题表达式10 简单谓词表达式10 量化表达式10 1.3.3具体 RSL 类型11 集合枚举11 笛卡尔枚举11 列表枚举12 映射枚举12 集合操作13 笛卡尔操作15 列表操作15 映射操作17 1.3.4 演算 + 函数19 演算句法19 自由与约束变量19 代入19 $\alpha $ 换名与 $\beta $ 规约20 函数基调20 函数定义20 1.3.5其他应用表达式21 let 表达式21 条件表达式22 操作符/操作数表达式23 1.3.6命令式结构24 变量与赋值24 语句序列与 \bf skip24 命令式条件语句24 循环条件语句24 迭代序列25 1.3.7进程结构25 进程通道25 进程复合25 输入/输出事件26 进程定义26 1.3.8简单 RSL 规约26 1.4文献评注27 part II 规约刻面29 xpart规约刻面29 chapter 2层次与复合31 2.1关键问题31 2.1.1非形式说明31 2.1.2形式说明32 2.2初步的方法论的结论33 2.2.1一些定义33 层次抽象33 “自顶向下”33 “自底向上”33 2.2.2原则与技术33 2.3主要的例子34 2.3.1层次的叙述表示34 2.3.2层次的形式表示36 2.3.3复合的，叙述性表示39 2.3.4复合的形式表示41 2.4讨论43 2.5文献评注：Stanis\l aw Leshniewski43 2.6练习43 chapter 3指称和计算47 3.1前言47 3.1.1计算和指称47 3.1.2句法和语义48 3.1.3特性描述48 3.2指称语义48 3.2.1一个简单的例子：数符48 3.2.2指称原则49 3.2.3表达式指称50 一个扩展52 3.2.4GOTO 连续53 问题54 句法类型56 语义类型57 主要的语义函数58 程序58 块58 一个深奥的问题59 例 3.3\hbox 的其他评论60 其余的语义函数60 赋值60 语句列表60 条件 GOTO61 while 循环61 讨论61 3.2.5指称语义的讨论61 3.3计算语义63 3.3.1关键问题63 3.3.2两个例子63 3.3.3表达式计算63 计算状态64 引出控制栈的动机64 细化函数65 讨论66 3.3.4GOTO 程序的计算语义66 句法66 一些语义观测结果67 观测 167 观测 267 语义类型68 解释器函数68 3.3.5协同例程程序的计算语义71 “协同例程”程序文本 I71 协同例程程序文本 II72 3.3.6讨论72 有关连续的机械化73 有关通过标号变量的 GOTO 的“威力”73 有关计算语义73 3.4回顾：指称和计算73 3.5一些语义的创始人74 3.5.1John McCarthy74 3.5.2Peter Landin75 3.6练习76 chapter 4格局：上下文和状态79 4.1引言80 4.2问题82 4.3“现实世界”上下文和状态83 4.3.1物理系统：上下文和状态83 4.3.2上下文和状态84 4.3.3非物理系统：上下文和状态84 上下文84 状态85 模型85 4.3.4讨论，I85 4.3.5讨论，II86 4.4第一次总结：上下文和状态86 4.4.1概述86 模型和规约状态86 4.4.2开发原则和技术87 4.5程序设计语言格局87 4.6并发进程格局87 4.6.1示例87 一句提示88 4.2(a) 语义的注释89 4.2(b) 语义的注释89 4.2(c) 语义的注释89 4.2(d) 语义的注释89 4.6.2总结92 4.7第二次总结：上下文和状态93 4.8信息状态和行为状态93 4.8.1作为状态机数据的程序流程图94 4.8.2流程图 $\equiv $ 机器94 4.8.3流程图机94 4.8.4评论95 4.8.5结论95 4.9最后的总结：上下文和状态96 4.10练习97 part\ III\hskip 关键领域和系统刻面99 xpart关键领域和系统刻面99 chapter 5时间、空间和空间/时间101 5.1时间101 5.1.1时间 ------ 基础102 时间变化实体 = 动态实体102 时间和动态性104 5.1.2时间 ------ 一般问题104 5.1.3时间的 \CJKfamily kai“A 序列”和 \CJKfamily kai“B 序列”模型104 5.1.4时间的连续统理论105 5.1.5时态事件106 5.1.6时态行为106 5.1.7时间表示106 5.1.8时间“上”的操作108 5.2空间108 5.2.1空间 ------ 基础108 5.2.2位置变化实体109 5.2.3位置和动态性110 5.2.4空间 ------ 一般问题111 点、曲线、曲面、体积111 空间“事件”111 空间“行为”112 空间体的表示112 空间上的操作112 5.3空间/时间113 5.3.1指导示例113 5.3.2空间/时间的表示114 5.3.3Blizard 的时间空间理论114 \CJKfamily kaiBlizard 空间/时间模型讨论115 5.4讨论115 5.5文献评注115 5.6练习115 part\ IV\hskip 语言学119 xpart语言学119 chapter 6语用121 6.1前言121 6.2日常语用122 6.3“形式”语用122 6.4讨论123 6.4.1概述123 6.4.2原则和技术123 6.5文献评注123 6.6练习124 chapter 7语义126 7.1前言126 7.2具体语义127 7.3“抽象”语义127 7.4预备语义概念127 7.4.1句法和语义类型127 7.4.2上下文128 7.4.3状态128 7.4.4格局128 7.4.5解释、求值、细化128 7.5指称语义129 7.5.1简单情况130 7.5.2复合情况130 7.6宏扩展语义130 7.6.1重写131 7.6.2宏扩展131 7.6.3归纳重写132 静态归纳语义132 动态归纳语义133 7.6.4不动点求值134 7.7操作和计算语义135 7.7.1栈语义135 7.7.2属性语法语义135 符号属性语法解析树示例138 7.8证明规则语义139 7.9讨论141 7.9.1概述141 7.9.2原则、技术和工具141 7.10文献评注142 7.11练习142 chapter 8句法145 8.1问题145 8.1.1形式和内容：句法和语义145 8.1.2本章的结构和内容146 8.2句子和语义结构146 8.2.1概述147 句子结构的句法147 语义结构的句法147 8.2.2句子结构示例147 简单句子结构的建模148 8.2.3语义结构示例149 8.3第一个抽象句法，John McCarthy152 8.3.1分析语法：观测器和选择器152 8.3.2合成语法：生成器153 8.4 BNF 语法 $\approx $ 具体句法153 8.4.1 BNF 语法154 8.4.2 BNF$\leftrightarrow $ RSL 语法解析树关系154 8.5结构生成器和识别器156 8.5.1上下文无关语法和语言156 8.5.2语法解析树157 8.5.3正则表达式和语言159 8.5.4语言识别器160 8.6XML：可扩展标记语言（Extensible Markup Language）160 8.6.1例160 8.6.2讨论162 8.6.3历史背景162 8.6.4目前的 XML“狂热”162 8.6.5 XML 表达式162 8.6.6 XML 模式164 8.6.7参考166 8.7抽象句法166 8.7.1存储模型的抽象句法166 值和值的类型167 位置和位置类型167 存储168 类型约束168 8.7.2其他存储模型的抽象句法169 非形式阐述169 形式说明170 8.8转换 RSL 类型到 BNF170 8.8.1问题170 8.8.2可能的解决办法171 8.9非形式和形式句法讨论172 8.9.1概述172 8.9.2原则、技术和工具172 8.10文献评注173 8.11练习173 chapter 9符号体系180 9.1符号体系 = 句法 $\oplus $ 语义 $\oplus $ 语用180 9.2符号体系181 9.3语言构件181 9.4语言学182 9.5语言和系统183 9.5.1职业语言183 9.5.2元语言184 9.5.3系统184 物理系统角度184 物理和非物理系统的例子185 语言系统角度186 示例系统语言187 流程图语言191 简单流程图的非形式句法191 简单流程图192 简单流程图的形式句法192 结构化流程图193 系统图和形式规约194 9.5.4系统图语言195 9.5.5系统概念讨论196 9.5.6作为语言的系统196 9.6讨论197 9.6.1概述197 9.6.2原则、技术和工具197 9.7Charles Sanders Peirce197 9.8文献评注197 9.9练习198 part\ V\hskip 其他规约技术203 xpart其他规约技术203 chapter 10模块化205 10.1前言206 10.1.1一些示例206 示例回顾210 模块描述：对象和模式210 实现210 逐步开发211 关注分离211 10.1.2预备性讨论211 软件设备211 抽象数据类型 $\DOTSB \mapstochar \rightarrow $ 代数语义211 框架方法212 实体关系图（Entity-Relationship，ER）212 模块化的一般语用213 模块化的一般语义213 模块化的一般句法213 一般的模块规约方法213 10.1.3章节结构213 10.2 RSL 类、对象和模式213 10.2.1介绍 RSL “类”概念214 RSL 声明的意义 ------回顾214 RSL\ “类”概念的第一个动机：关注焦点214 RSL\ “类”概念的第二个动机：语义代数214 RSL\ “类”概念的第三个动机215 RSL\ “类”概念的第四个动机：命名模式216 10.2.2 RSL\ “类”概念217 10.2.3 RSL “对象”概念218 10.2.4 RSL\ “模式”概念218 简单模式218 模式扩展219 隐藏220 其他223 10.2.5 RSL\ “模式”参数化223 动机：模式为什么和如何参数化？223 参数化模式的句法和语义225 10.2.6“大型”示例226 对比背景示例226 叙述226 形式化226 模式化示例228 10.2.7定义：类、模式和对象230 10.3UML 和 RSL231 10.3.1 UML 图概述231 用例图231 序列/合作图232 状态图232 10.3.2类图232 UML “标准化”232 10.3.3类图232 类232 关联233 连接234 泛化235 10.3.4例：铁路网235 10.3.5比较 UML 和 RSL OO 结构236 10.3.6引用237 10.3.7类图的限制237 10.4讨论238 10.4.1模块性问题238 模块规约和程序设计238 模块性概念的稳定性238 面向对象（ Object-Oriented，OO）“程序设计”何去何从238 模式、对象和模块演算238 UML 类图概念的形式化239 10.4.2原则、技术和工具239 10.5文献评注239 10.6练习239 chapter 11自动机和机器241 11.1离散状态自动机241 11.1.1直观理解243 11.1.2动机243 11.1.3语用243 11.2离散状态机器245 11.3有限状态自动机246 11.3.1正则表达式语言识别器246 11.3.2正则表达式247 11.3.3形式语言和自动机248 11.3.4自动机完全化248 11.3.5非确定性自动机248 11.3.6最小状态有限自动机249 11.3.7有限状态自动机形式化， I250 11.3.8有限状态自动机实现，I250 11.3.9有限状态自动机形式化，II251 11.3.10有限状态自动机实现，II252 11.3.11有限状态自动机 ------ 总结252 11.4有限状态机器253 11.4.1有限状态机器控制器253 11.4.2有限状态机器语法分析器255 11.4.3有限状态机器形式化256 11.4.4有限状态机器实现257 11.4.5有限状态机器 ------ 总结258 11.5下推栈设备259 11.5.1下推栈自动机和机器259 11.5.2下推栈机器形式化260 11.5.3下推栈设备总结262 11.6文献评注：自动机和机器262 11.7练习262 part\ VI\hskip 并发和时态265 xpart并发和时态265 chapter 12佩特里网267 12.1问题267 12.2条件事件网（Condition Event Net，CEN）268 12.2.1描述268 12.2.2CEN 小示例268 12.2.3条件事件网的 RSL 模型271 CEN 句法和静态语义271 动态语义273 12.3位置变迁网（Place Transition Net，PTN）273 12.3.1描述274 12.3.2PTN 小例子274 12.3.3位置变迁网的 RSL 模型275 PTN 句法和静态语义275 动态语义276 12.3.4铁路领域佩特里网示例278 进路（route）描述278 联锁表278 单元的佩特里网279 转辙器的佩特里网280 信号的佩特里网280 进路的佩特里网280 联锁表佩特里网的构造281 进路和单元281 进路和转辙器281 进路和信号281 总结281 12.4染色佩特里网（Coloured Petri Net，CPN）282 12.4.1描述282 12.4.2CPN 示例283 12.4.3染色佩特里网 RSL 模型285 CPN 句法和静态语义285 染色佩特里网的动态语义287 辅助语义函数287 染色佩特里网的变迁函数288 12.4.4时间化染色佩特里网289 12.5CEN 示例：工作流系统290 12.5.1项目计划290 项目计划290 项目计划构造292 12.5.2项目活动293 项目控制流：“波”和迹293 项目计划“执行”295 12.5.3项目生成300 进程生成300 通道分配301 12.6CPN 和 RSL 示例：超标量处理器302 12.6.1描述302 12.6.2染色佩特里网303 12.6.3 RSL\ 模型：超标量处理器308 12.7讨论316 12.8文献评注317 12.9练习317 chapter 13消息和活序列图319 paragraph\textup 读者指南319 13.1消息序列图319 13.1.1问题319 13.1.2基本 MSC（Basic MSC，\textrm BMSC）320 非形式阐述320 BMSC 示例323 \textrm BMSC 句法的 RSL 模型324 13.1.3高级 MSC（High-Level MSC，\textrm HMSC）326 非形式阐述326 HMSC 示例326 13.1.4\textrm HMSC 句法的 RSL 模型326 13.1.5MSC 是 HMSC327 13.1.6MSC 的句法良构性328 13.1.7示例：\textrm IEEE 802.11 无线网络333 描述333 IEEE 802.11 示例的 RSL 模型336 13.1.8基本消息序列图的语义342 13.1.9高级消息序列图的语义343 13.2活序列图：非形式阐述344 13.2.1活序列图句法344 活序列图的图形句法344 全称和存在图344 前图（Prechart）344 “热”和“冷”消息345 同步和异步消息345 条件345 子图346 位置347 13.2.2活序列图示例，I348 13.3进程代数350 13.3.1进程代数 \ensuremath \mathit PA_\epsilon 350 基调350 等式351 可导出性352 归约到基本项353 13.3.2 \ensuremath \mathit PA_\epsilon 语义356 13.3.3进程代数 $PAc\@uscore .\epsilon $359 13.3.4 \ensuremath \mathit PAc_\epsilon 的语义361 13.4活序列图的代数语义364 13.4.1活序列图的文本句法364 13.4.2活序列图语义364 13.4.3活序列图实例，II368 13.5关联消息图到 RSL368 13.5.1集成的类型368 13.5.2 RSL 子集369 句法369 有通信行为的操作语义369 13.5.3关联活序列图到 RSL371 句法限制371 满足关系372 13.5.4检查满足性377 13.5.5工具支持378 13.6通信事务进程（Communicating Transaction Processes，CTP）379 13.6.1直观理解379 13.6.2\textup 阐述 CTP380 \textup CTP 图380 \textup CTP 进程380 \textup CTP 事务模式381 \textup CTP 事务图382 \textup 简单 CTP 消息序列图382 \textup 使能的 CTP 事务图383 \textup 使能的和被调用的模式和图383 详述调用和执行383 \textup CTP 变迁384 13.6.3哲学家就餐示例385 13.6.4\textup CTP 形式化388 \textup 句法和一些语义类型388 \textup 辅助句法和语义函数基调389 \textup 辅助函数基调和定义390 \textup CTP 的良构性390 \textup 图的良构性392 \textup 动态语义，类型394 paragraph\textup 语义类型394 paragraph\textup 良构性395 \textup 动态语义，函数396 paragraph\textup 辅助函数396 paragraph\textup 初始化398 paragraph\textup 使能398 paragraph\textup 激活399 13.7讨论401 13.7.1概述401 13.7.2原则、技术和工具402 13.8文献评注402 13.9练习403 chapter 14状态图406 14.1前言406 14.2状态图的描述407 14.3状态图句法的 RSL 模型411 14.4例413 14.4.1铁路线路自动闭塞414 叙述414 一般线路段414 第一线路段416 状态图416 一般模型416 特殊情况416 14.4.2铁路线路方向协议系统418 叙述418 LDAS 内部行为（状态图）420 车站 A 的内部状态（状态图）421 车站 B 的内部行为（状态图）421 外部行为（活序列图）421 14.4.3无线雨量计422 描述422 状态图模型423 RSL\ 模型424 14.5状态图的进程代数427 14.5.1SPL（Statechart Process Language）: 状态图进程语言428 14.5.2SPL 语义428 14.5.3SPL 项等价429 14.6状态图语义430 14.6.1状态图的 SPL 语义430 14.6.2状态图示例433 14.7关联状态图到 RSL433 14.7.1句法限制433 14.7.2满足关系435 14.7.3满足检查435 14.7.4工具支持436 14.8讨论436 14.8.1概述436 14.8.2原则、技术和工具436 14.9文献评注437 14.10练习437 paragraph\textup 数字钟状态：441 paragraph\textup 时间/日期更新状态：441 paragraph\textup 闹铃更新状态：441 paragraph\textup 跑表状态：441 paragraph\textup 数字钟的高级描述：442 chapter 15时间的定量模型443 15.1问题443 15.1.1软时态443 15.1.2硬时态444 15.1.3软实时和硬实时444 15.1.4例子 ------“老方法”！444 15.1.5本章的结构445 15.2时态逻辑446 15.2.1问题446 15.2.2哲学语言学背景446 15.2.3区间时态逻辑 451 15.2.4经典时态操作符 452 15.3时段演算452 15.3.1例子，第 I 部分453 15.3.2一些基础概念453 布尔状态、状态断言和特性函数453 状态时段454 什么是煤气灶？454 煤气泄漏455 煤气灶需求456 15.3.3例子，第 II 部分456 问题描述456 构件456 属性457 事件457 行为457 不变式458 需求： L\_Req458 基础模型458 形式需求458 15.3.4句法459 简单表达式459 状态表达式和断言460 时段和时段项460 时段公式460 通常的时段公式简写460 15.3.5非形式语义461 15.3.6例子，第 III 部分462 电梯例子：设计462 软件设计， L\_Design462 领域描述：假设， L\_Domain463 简单设计相对于领域和需求的正确性464 公路铁路水平交叉口例子464 问题描述465 形式化465 \CJKfamily kai[1] 状态变量465 \CJKfamily kai[2] 需求466 \CJKfamily kai[2.1] 安全需求467 \CJKfamily kai[2.2] 功能需求467 问题描述468 火车接近470 火车通过470 一些观察470 评论470 关于验证和模型检测的问题471 15.3.7变迁和事件471 15.3.8讨论：从领域到设计475 15.4 TRSL: 具有时间的 RSL475 15.4.1 TRSL 的设计标准476 第一个 TRSL 设计决策476 第二个 TRSL 设计决策476 15.4.2 TRSL 语言478 句法478 语义478 15.4.3另一个煤气灶的例子479 15.4.4讨论482 15.5具有时间和时段的 RSL482 15.5.1 TRSL 的回顾482 15.5.2 TRSL 和时段演算483 问题描述484 时段演算需求484 TRSL 规约484 满足关系485 15.6讨论485 15.6.1一般问题485 15.6.2原则、技术和工具486 15.7文献评注486 15.8练习487 part\ VII\hskip 解释器和编译器定义489 xpart解释器和编译器定义489 chapter 16SAL：简单应用式语言491 16.1提示491 16.2\textrm SAL 句法492 16.2.1\textrm SAL 句法的非形式说明492 16.2.2\textrm SAL 句法的形式说明492 16.2.3评论493 16.3指称语义493 16.3.1非形式语义493 16.3.2形式语义494 语义类型494 操作符意义494 语义函数495 16.3.3\textrm SAL 语义的回顾，1495 16.3.4两句题外话496 后面的内容!496 最近的错误496 16.4一阶应用式语义498 16.4.1句法类型498 16.4.2语义类型498 16.4.3抽象函数499 16.4.4辅助函数500 16.4.5语义函数500 16.4.6回顾503 16.4.7\textrm SAL 语义的回顾，2503 16.5抽象命令式栈语义504 16.5.1设计决策 ------ 非形式动机说明504 16.5.2语义风格评论504 16.5.3句法类型505 16.5.4语义类型505 16.5.5抽象函数505 16.5.6运行时函数505 16.5.7语义函数507 两个不变式507 [0] 解释程序507 前一步骤：507 当前步骤：507 [1] 解释常量表达式508 前一步骤：508 当前步骤：508 [2] 解释变量表达式508 前一步骤：508 当前步骤：508 [3] 解释前缀表达式509 前一步骤：509 当前步骤：509 [4] 解释中缀表达式509 前一步骤：509 当前步骤：509 [5] 解释条件表达式510 前一步骤：510 当前步骤：510 [6] 解释 lambda 表达式510 前一步骤：510 当前步骤：510 [7] 解释简单 let 表达式510 前一步骤：510 当前步骤：511 [8] 解释递归 let 表达式511 前一步骤：511 当前步骤：511 [9] 解释函数应用表达式511 前一步骤：511 当前步骤：512 16.5.8\textrm SAL 语义的回顾，3512 16.6宏扩展语义512 16.6.1栈语义分析513 非形式设计描述516 [1] 运行时状态516 [2] 宏扩展516 [3] 闭包的实现517 [4] 编译状态 ------ 编译时规约517 [5] 编译状态 ------ 字典517 执行518 16.6.2句法类型519 16.6.3编译时类型519 16.6.4运行时语义类型519 16.6.5运行时状态520 16.6.6运行时栈操作520 16.6.7运行时栈搜索变量值520 16.6.8宏扩展函数521 [0] 程序宏扩展521 前一步骤：521 当前步骤：522 [1] 常量表达式宏扩展522 前一步骤：522 当前步骤：522 [2] 变量表达式宏扩展522 前一步骤：522 当前步骤：522 [3] 前缀表达式宏扩展523 前一步骤：523 当前步骤：523 [4] 中缀表达式宏扩展523 前一步骤：523 当前步骤：523 [5] 条件表达式宏扩展524 前一步骤：524 当前步骤：524 [6] lambda 表达式宏扩展524 前一步骤：524 当前步骤：524 [7] 简单 Let 表达式的宏扩展525 前一步骤：525 当前步骤：525 块宏扩展525 [8] 递归函数/Let 表达式宏扩展527 前一步骤：527 当前步骤：527 [9] 函数应用表达式宏扩展528 前一步骤：528 当前步骤：528 16.6.9\textrm SAL 语义的回顾，4528 16.7ASM：一个汇编语言529 16.7.1语义类型529 16.7.2计算机状态530 16.7.3地址概念530 16.7.4机器指令530 16.7.5机器语义532 解释代码532 确定标号索引533 立即存储和存储指令533 立即装入和装入指令533 应用函数指令534 无条件转移指令536 条件转移指令536 寄存器传送和调整指令537 封装和解封装指令537 输出指令537 结束指令538 16.7.6ASM 的回顾538 16.8一个编译算法538 16.8.1句法类型539 16.8.2编译时类型和状态539 16.8.3编译时动态函数539 16.8.4编译时静态函数539 16.8.5运行时常量值540 16.8.6编译函数540 [0] 程序编译540 前一步骤：540 当前步骤：541 [1] 常量表达式编译541 前一步骤：541 当前步骤：541 [2] 变量表达式编译541 前一步骤：541 当前步骤：542 [3] 前缀表达式编译543 前一步骤：543 当前步骤：543 [4] 中缀表达式编译543 前一步骤：543 当前步骤：543 [5] 条件表达式编译543 前一步骤：543 当前步骤：544 [6] Lambda 表达式编译544 前一步骤：544 当前步骤：544 [7] 简单 Let 表达式编译545 前一步骤：545 当前步骤：545 [*] 块表达式545 前一步骤：545 当前步骤：546 [8] 递归函数/Let 表达式编译546 前一步骤：546 当前步骤：547 [9] 函数应用表达式编译547 前一步骤：547 当前步骤：548 16.8.7编译算法的回顾548 16.9一个属性语法语义548 16.9.1抽象句法类型549 16.9.2\textrm SAL BNF 语法，1549 16.9.3结点属性550 16.9.4常量550 16.9.5一些排印区别550 16.9.6编译函数550 [0] 程序编译550 [1] 常量表达式编译550 [2] 变量表达式编译550 前一步骤：551 当前步骤：551 [3] 前缀表达式编译551 [4] 中缀表达式编译551 [5] 条件表达式编译551 [6] lambda 表达式编译551 前一步骤：552 当前步骤：552 前一步骤：552 当前步骤：552 [7] 简单 let 表达式编译552 前一步骤：553 当前步骤：553 前一步骤：553 当前步骤：553 [*] 块表达式编译553 前一步骤：554 当前步骤：554 [8] 递归函数/let 表达式编译554 [9] 函数应用表达式编译554 前一步骤：555 当前步骤：555 16.9.7属性语义回顾，1555 前一步骤：556 当前步骤：556 16.10另一个属性语法语义556 前一步骤：557 当前步骤：557 16.10.1抽象句法类型557 16.10.2\textrm SAL BNF 语法，2557 前一步骤：558 当前步骤：558 16.10.3全局变量558 前一步骤：559 当前步骤：559 16.10.4常量559 16.10.5结点属性560 16.10.6编译函数560 [0] 程序编译560 [1] 常量表达式编译560 [2] 变量表达式编译560 [3] 前缀表达式编译560 [4] 中缀表达式编译560 前一步骤：561 当前步骤：561 前一步骤：561 当前步骤：561 [5] 条件表达式编译561 [6] lambda 表达式编译561 前一步骤：562 当前步骤：562 前一步骤：562 当前步骤：562 [7] 简单 let 表达式编译562 [$\bullet $] 块表达式编译562 前一步骤：563 当前步骤：563 [8] 递归函数/let 表达式编译563 [9] 函数应用表达式编译563 16.10.7属性语义的回顾，2563 16.11讨论563 16.11.1概述563 前一步骤：564 当前步骤：564 前一步骤：565 当前步骤：565 16.11.2原则、技术和工具565 前一步骤：566 当前步骤：566 16.12回顾和文献评注566 前一步骤：567 当前步骤：567 前一步骤：568 当前步骤：568 前一步骤：569 当前步骤：569 16.13练习569 chapter 17SIL：简单命令式语言571 17.1背景571 17.2句法类型572 17.2.1具体的模式性句法573 17.2.2抽象句法573 17.3命令式指称语义573 17.3.1语义类型574 17.3.2辅助语义函数574 17.3.3语义函数574 过程指称574 语句和表达式函数575 17.4宏扩展语义575 17.4.1句法类型576 17.4.2编译时语义类型576 17.4.3运行时语义类型576 运行时状态“快照”576 语义类型577 17.4.4运行时状态声明和初始化577 17.4.5抽象函数578 17.4.6宏578 17.5讨论580 17.5.1概述580 17.5.2原则、技术和工具580 17.6文献评注580 17.7练习581 chapter 18SMIL：简单模块命令式语言583 18.1句法类型583 18.2指称语义584 18.2.1语义类型584 18.2.2辅助函数584 静态函数584 时态函数585 18.2.3语义函数585 语义函数类型585 语义函数定义586 18.3宏扩展语义586 18.3.1运行时语义类型587 18.3.2编译/运行时语义类型587 18.3.3编译时语义类型588 18.3.4语义函数589 18.4讨论590 18.4.1概述590 18.4.2原则、技术和工具590 18.5文献评注591 18.6练习591 chapter 19SPIL：简单并行命令式语言586 19.1问题586 19.2句法586 19.2.1非形式句法587 进程表达式587 表达式和语句587 系统进程588 19.2.2形式句法588 19.3进程概念和语义类型589 19.3.1句法概念589 文本的589 上下文的：作用域和绑定590 上下文的：隐藏和模块化590 19.3.2机器和解释器590 19.3.3语义概念和类型590 动作590 进程591 对象591 环境 $\rho :$ENV ------ I591 存储 $\sigma :\Sigma $591 19.4面向进程的语义类型591 19.4.1唯一进程标识符 $\pi :\Pi $592 19.4.2堆 $\xi :\Xi $592 19.4.3输入/输出通道绑定593 19.4.4环境 $\rho :$ ENV594 19.4.5状态复合 594 全局状态595 19.5初始和辅助语义函数595 19.5.1开始函数595 19.5.2系统函数596 19.5.3绑定和分配函数596 19.5.4自由和绑定函数597 19.5.5分配函数597 19.5.6变迁循环598 19.6语义函数598 19.6.1 \CJKfamily kai下一状态变迁函数598 19.6.2赋值语句598 19.6.3\sl case 语句599 19.6.4\sl while 循环599 19.6.5\sl repeat until 循环600 19.6.6简单输入/输出进程600 19.6.7并行进程命令 601 19.6.8 \CJKfamily kaistop 进程技术细节601 19.6.9进程 \CJKfamily kaicall 命令602 19.6.10内部非确定性进程， 602 19.6.11外部非确定性进程 602 19.6.12非确定性输入/输出进程603 19.6.13嵌入式系统进程命令603 19.6.14 \CJKfamily kaifinish 进程技术细节604 19.7讨论604 19.7.1概述604 19.7.2原则、技术和工具604 19.8文献评注605 19.9练习605 part\ VIII\hskip 结束语609 xpart结束语609 chapter 20结束语611 20.1总结611 20.2结论：卷 1 和 2611 20.3卷 3 的预览612 20.4“UML”化形式技术613 part\ IX\hskip 附录615 xpart附录615 chapter命名规则617 chapter参考文献621 样章： 023237-01.pdf 课件： 网络资源： 配套教学用书（配套教参、主课本等）： ·软件工程卷1：抽象与建模 ·软件工程卷3：领域、需求与软件设计 可替代教学用书： 丛书名称：世界著名计算机教材精选 图书书评：

【欢迎来稿】 总编办：c-service@tup.tsinghua.edu.cn  【选题意向登记表】

客户服务：（010）62776969 c-service@tup.tsinghua.edu.cn

教师服务电话：010-62770175-3506

反盗版举报电话：(010) 62782989 bairsh@tup.tsinghua.edu.cn

质量反馈：(010) 62772015 zhiliang@tup.tsinghua.edu.cn

邮购电话：(010) 62786544 e-sale@tup.tsinghua.edu.cn

邮购地址：北京市海淀区清华大学出版社邮购组收 邮编:100084

读者服务部（购书）：(010) 62781733

通讯地址：清华大学学研大厦 A 座 邮编：100084

网管信箱：netadmin@tup.tsinghua.edu.cn

版权所有(C)2005 清华大学出版社有限公司

Copyrights @ 2005 by Tsinghua University Press. All Rights Reserved 京ICP备 05029640 号