描述
软件工程中形式方法导论，涵盖命题与一阶逻辑（语法、语义、证明论）、形式规范语言、有界分析与验证、形式规范工具，以及使用有限状态机、时序逻辑和模型检验工具的模型检验。
先修课程
- 先修科目：COMP 1805 ，SYSC 3120 ，和 SYSC 4001 。
条件与方式
- 先修科目：COMP 1805 ，SYSC 3120 ，和 SYSC 4001 。
- 每周讲课三小时。
原文参考文本
Introduction to formal methods in software engineering with coverage of propositional and first-order logic (syntax, semantics, proof theory), formal specification languages, bounded analysis and validation, formal specification tools, and model checking with finite-state machines, temporal logic, and model checking tools.
- Prerequisite(s): COMP 1805 , SYSC 3120 , and SYSC 4001 .
- Lectures three hours a week.
来源与参考
为帮助您核实信息，保留了日期和来源。为便于阅读提供了翻译；以官方来源为准，查看条件和要求。
来源参考 : https://calendar.carleton.ca/undergrad/courses/SYSC/