课程名称:程序设计形式语义学
课程名称：程序设计形式语义学
英文名称：The Formal Semantics of Program
一、课内学时： 32 学分： 2
二、适用专业：
计算机科学与技术
三、预修课程；
离散数学，程序设计语言
四、教学目的：
为了适应计算机科学技术的迅速发展和对系统研发人才的要求，计算机专业的研究生有必要在深入学习专业知识的同时，对程序形式语义学有一个全面的了解，以便掌握程序设计语言的两个必要组成部分：语言的形式语法和形式语义。
本课程的内容是程序设计理论的组成部分，它以数学为工具，利用符号和公式，精确地定义和解释计算机程序设计语言的语义。通过本课程的学习，使学生在计算机语言的形式语义学方面打下扎实的基础，掌握形式语义学的基本理论、基本方法和重要结论，并了解国内外最新研究动态、热点，为以后的研究做好准备。
五、教学方式：
课堂讲授为主，学生讨论为辅，此外还包括25%的实验内容（基于Hoare 公理化方法的公理语义证明）。
六、教学主要内容及对学生的要求：
1 语义、真值与逻辑
1.1 命题、句义和话语义
1.2 句义的信息类型
1.3 程序形式语义学的研究范围、
1.4 逻辑在语义研究中的地位
2 指称语义
2.1 指称语义的基础
2.2 存储语义
2.3 环境语义
2.4 命令语义
2.5 指称语义举例
3 操作语义
3.1 程序的结构化操作语义与属性文法
3.2 施用表达式的机器计算
4 公理语义
4.1 Hoare公理系统
4.2 Dijkstra的最弱前置条件
4.3 Martin-Lof类型论
4.4 程序正确性证明方法
5 并发程序设计语言的语义
5.1 并发系统
5.2 并发程序设计语言及其指称语义和公理语义
5.3 通讯顺序进程及其操作语义
6 辅助性形式语义描述实例应用
7 基于Hoare 公理化方法的公理语义证明实验
7.1 Hoare公理化规则的编程实现
7.2 待证程序的语义性质P （前置条件）和Q （后置条件）的描述
7.3 逻辑式的推导和验证
要求学生查阅国内外相关技术资料并阅读参考文献，做好课程的技术讨论环节。
七、参考书及学生必读参考资料：
主要参考书目:
1. 《程序设计语言理论基础》，许满武等译. 北京：电子工业出版社. 2006.
2. 《程序设计语言的形式语义》，宋国新等译. 北京：机械工业出版社. 2005.
3. 《形式语义学的稳定论域理论》，陈仪香 著. 北京:科学出版社. 2003. 学生必读参考书籍:
1. 《程序设计方法学》，李传湘 著. 武汉:武汉大学出版社. 2002.
八、大纲撰写人：张琨
九、任课教师：张琨