南京理工大学
《程序设计形式语义学》课程内容简介
课程编码 S106B007 课程类别 必修课
课程名称 程序设计形式语义学
英文名称 The Formal Semantics of Program
开课院系 计算机科学与工程学院
开课季节 秋学期 授课方式 面授讲课
考核方式 考试 课件地址
考试方式 闭卷 成绩计算方法 期末100%
课程总学时 32 课程学分 2
实验学时 适用对象
课程类型 理论课 课程属性 必修
任 课 教 师
教师姓名性别所属院系职称年龄
朱保平 计算机科学与工程学院 副教授 57

教学目标:
为了适应计算机科学技术的迅速发展和对系统研发人才的要求,计算机专业的研究生有必要在深入学习专业知识的同时,对程序形式语义学有一个全面的了解,以便掌握程序设计语言的两个必要组成部分:语言的形式语法和形式语义。
本课程的内容是程序设计理论的组成部分,它以数学为工具,利用符号和公式,精确地定义和解释计算机程序设计语言的语义。通过本课程的学习,使学生在计算机语言的形式语义学方面打下扎实的基础,掌握形式语义学的基本理论、基本方法和重要结论,并了解国内外最新研究动态、热点,为以后的研究做好准备。

课程内容:
1  语义、真值与逻辑  (2学时)
1.1 命题、句义和语义
1.2 句义的信息类型
1.3 程序形式语义学的研究范围*
1.4 逻辑在语义研究中的地位*
2  指称语义(4学时)
2.1 指称语义的基础*
2.2 存储语义
2.3 环境语义
2.4 命令语义
2.5 指称语义举例*
3  操作语义 (6学时)
3.1 程序的结构化操作语义与属性文法
3.2 施用表达式的机器计算*#
4  公理语义 (8学时)
4.1 Hoare公理系统*
4.2 Dijkstra的最弱前置条件*#
4.3 Martin-Lof类型论*#★
4.4 程序正确性证明方法*#
5  并发程序设计语言的语义(6学时)
5.1并发系统
5.2 并发程序设计语言及其指称语义和公理语义*  
5.3 通讯顺序进程及其操作语义*#
6  辅助性形式语义描述实例应用★(2学时)
7  基于Hoare公理化方法的公理语义证明实验(4学时)
7.1 Hoare公理化规则的编程实现
7.2 待证程序的语义性质P(前置条件)和Q(后置条件)的描述
7.3 逻辑式的推导和验证 *#

适用学生:
全日制硕士    非全日制硕士    留学硕士    进修硕士    硕博连读    本科直博    全日制博士    留学博士    进修博士    在职专硕    其他    

预修课程:
预修课程:
离散数学、程序设计语言、数据结构

参考书目:
教材:(美)米切尔箸.许满武等译.程序设计语言理论基础.北京:电子工业出版社,2006.
参考书:
[1]李传湘,陈世鸿,刘海青.程序设计方法学.武汉:武汉大学出版社,2000.
[2] 陈意云.形式语义学基础.合肥:中国科学技术大学出版社,1994
参考资料:
Glynn Winskel箸.宋国新等译.程序设计语言的形式语义.北京:机械工业出版社,2004.

备注: