课程简介 计算机科学的理论体系 1、模型理论 ●关心的问题 -给定模型M, 哪些问题可以由模型M解决 -如何比较模型的表达能力 经典计算 确定的图灵机，可计算性理论属于模型理论 新型计算 本质特点是交互（并发、分布、网络、网格、云〉 ·计算和交互的统一模型理论尚未出现
课 程 简 介 计算机科学的理论体系 1、模型理论 • 关心的问题 – 给定模型M，哪些问题可以由模型M解决 – 如何比较模型的表达能力 • 经典计算 – 确定的图灵机，可计算性理论属于模型理论 • 新型计算 – 本质特点是交互( 并发、分布、网络、网格、云 ) • 计算和交互的统一模型理论尚未出现
课程简介 计算机科学的理论体系 2、程序理论 。关心的问题 -给定模型M, 如何用模型M解决问题 ●包括的领域 -程序设计范型、 程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课 程 简 介 计算机科学的理论体系 2、程序理论 • 关心的问题 – 给定模型M，如何用模型M解决问题 • 包括的领域 – 程序设计范型、程序设计语言、程序设计、形式 语义、类型论、程序验证、程序分析等
课程简介 计算机科学的理论体系 3、计算理论 。关心的问题 给定模型M和一类问题，解决该类问题需要多少 资源 ●包括的领域 一计算复杂性理论
课 程 简 介 计算机科学的理论体系 3、计算理论 • 关心的问题 – 给定模型M和一类问题，解决该类问题需要多少 资源 • 包括的领域 – 计算复杂性理论
课程简介 作为编译原理的后续课程，可选内容列举： 独立于机器的优化（涉及，但不是重点》 一依赖于机器的优化（留给高级系统结构课程〉 -形式语义和类型论（程序设计语言理论课程） 各种语言范型的实现技术（不涉及》 一提高软件质量的方法 1、程序分析 2、形式验证 模型检测：对软件的数学模型进行系统地全面考察 程序验证：用形式方法对软件进行数学推理
课 程 简 介 作为编译原理的后续课程，可选内容列举： – 独立于机器的优化（涉及，但不是重点） – 依赖于机器的优化（留给高级系统结构课程） – 形式语义和类型论（程序设计语言理论课程） – 各种语言范型的实现技术（不涉及） – 提高软件质量的方法 1、程序分析 2、形式验证 模型检测：对软件的数学模型进行系统地全面考察 程序验证：用形式方法对软件进行数学推理
课程简介 本课程概述 学习程序分析和形式验证的基本原理，它们在高 可信软件、代码优化、并行编译等许多方面有广 泛应用 学习和讨论各类方法解决的问题、采用的技术、 理论特性、算法等，并说明这些方法之间的关系 和不同。这些方法本身跨越多种程序设计语言特 征
课 程 简 介 • 本课程概述 – 学习程序分析和形式验证的基本原理，它们在高 可信软件、代码优化、并行编译等许多方面有广 泛应用 – 学习和讨论各类方法解决的问题、采用的技术、 理论特性、算法等，并说明这些方法之间的关系 和不同。这些方法本身跨越多种程序设计语言特 征