课程介绍

软件工程建模与形式化方法是软件工程硕士专业学位的选修课程，该课程介绍如何使用函数式程序设计语言对软件系统进行建模，并借助计算机辅助证明系统证明软件符合期待的行为规约。 学生在学习本课程之后应当掌握如何使用本课程教授的工具开发一套可靠的关键软件系统，并深入理解本课程所教授方法的核心意涵，并做到融会贯通， 在未来的工作或研究中，即使不使用本课程所教授的工具，也能够使用本课程训练形成的思维习惯，使自己所开发的软件系统更加可靠。

先修课程

课程名 课程号
程序设计基础 M210002B
离散数学 C110001B
数据结构 M310002B
算法设计与分析 M210004B

课程组成员

姓名 电子邮箱 办公地点 答疑时间
李令昆（授课教师） kunkun (at) bjtu.edu.cn 逸夫教学楼YF西811 第1至16教学周每周二10:00~12:00

授课时间及地点

周次 时间 地点
第1教学周至第16教学周 周二19:00~20:50 逸夫教学楼YF609
点此查看暂定教学日程

教学内容

  1. 函数式程序设计：Haskell语言
  2. 逻辑基础：ZF集合论、科里霍华德对应与类型论、程序生成
  3. 指令式程序设计逻辑：霍尔逻辑、分离逻辑、依赖类型论、Dafny简介
  4. 应用案例介绍

教材及参考资料

本课程没有指定教材，但是课程内容参考了如下参考资料：

成绩分布与评分规则

本课程为百分制课程，按照《北京交通大学研究生课程管理规定》第二十一条之规定，获得60分及以上为通过课程考核并获得学分。成绩分布如下：

  1. 平时成绩60分：包含三次作业，各计20分，其中：
    • 作业1：函数式程序设计，学生需使用课程教授的函数式程序设计语言完成授课教师指定的题目。
    • 作业2：程序设计逻辑基础，学生需使用Coq系统完成授课教师指定的逻辑证明题目。
    • 作业3：算法验证，学生需使用Coq系统自行选择一个常见的算法进行验证。
  2. 期末考试40分：闭卷考试（不得携带教材、笔记，不得使用手机、笔记本电脑等电子设备），卷面成绩100分，共计120分钟。

课堂规则

  1. 出勤：本课堂期望学生出席全部课程。若学生无法出席课程，应持有学院出具的请假条或医生出具的书面证明，符合请假要求的，允许延期提交作业、延期参与随堂考试、缓考期末考试，延期的时间由授课教师酌情决定。授课教师有权在任意时间检查出勤情况，授课教师在检查出勤情况之后拒绝迟到学生的补出勤要求，未按规定出席课程者，一次扣减总成绩5分，不设封顶。
  2. 作业：提交作业的截止时间为公告的截止日期当日00:00分，即前一日的23:59:59（北京时间）。迟交一日的，得分减去所得分数的15%；迟交两日的，减去所得分数的30%；迟交三日及以上的不得分。为了保障学生的学习质量，我们将尽力在作业截止日期之后的一周内反馈作业成绩和尽可能详细的扣分说明。
  3. 重新评分：虽然我们每次力求精准的判断作业答案的正确性，但是错误有时也会发生，如果学生认为自己的作业评分有误，可以在作业成绩发布后的一周内通过课程平台提交重新评分申请。重新评分申请只能通过课程平台提交，通过邮件提交的不予受理，超出截止日期的重新评分申请不予受理。
  4. 重要公告：课程进展过程中的通知公告一般在KL教学平台上发布，一些紧急的通知会通过校内邮箱发给大家，请定期查看KL教学平台和查收邮件。
  5. 课程资料的使用授权：由于课程资料（讲义、作业等）尚不具备出版资质，同时课程资料中的内容也不完全符合完全原创性与商用许可的规范（例如图片可能来源于其它文献，同时也未征得原作者的商用许可）。因此课程资料仅限课堂内部使用，未经授课教师许可不得在课程进行过程中以及课程结束之后公开发布或分发给课堂之外的第三人。违反此项规定者，应当承担由此引发的各种法律后果，同时授课教师有权对其寻求纪律处理。
  6. 课程礼仪：学生在参与课程过程中应当符合课程礼仪。行为举止及言语应当符合日常行为规范，不得出现谩骂他人，故意影响他人学习的行为。不遵守课程礼仪情节严重的，取消考核资格。
  7. 课程平台：学生不得使用任何技术手段攻击课程平台，如果课程平台存在漏洞应及时与授课教师联系。同时，学生有义务保证自己的账号安全，并不得将自己的课程平台账号借与他人使用。否则由此引发的一切后果由学生本人承担。
  8. 免修：本课程不接受任何免修申请。
  9. 因病造成学习困难的特殊政策：本课堂致力于为全部同学提供一种平等的学习环境。因病而造成学习困难的，例如焦虑症、理解障碍、抑郁症、双相情感障碍、精神分裂症等，可以在学期中的任何时间凭医院的诊断证明寻求任课教师力所能及的额外帮助（包括但不限于：允许延期提交作业，降低作业难度等），但仍然需要遵守课程的学业诚信的相关规定，授课教师保证保护当事同学的隐私。

答疑和电子邮件

  1. 请讲究提问的艺术：答疑不是让老师替你写作业，如果你需要答疑，那么你需要首先对自己的问题先有一些思考，然后再跟老师和其他同学讨论。我们不会回答简单的“XXX题目怎么做？”这种提问，正确的提问方式应该是“XXX题目我的想法是XXX，但是因为XXX，我发现我的想法是不对的，请问我应该怎样去思考（或者我的想法有什么问题）？”。
  2. 所有答疑的问题必须先发送到课程平台的讨论区中，因为你有的问题可能别人也有，公开答疑过程可以提高答疑的效率。同时学生应当在提问之前仔细阅读其它同学已经提出的问题并查看下方的讨论和回答，避免重复提问。
  3. 针对于课程材料和作业的问题通过邮件提问一律不予回复，我们非常乐意回复关于其它内容的提问，例如请假、寻求专业建议等。同时，永远不要发类似“老师我就差1分就90分了，我还有什么办法可以得到这一分？”的邮件，这是不合适的。
  4. 未在课程平台的讨论区提问的而直接在答疑时间来办公室提问的，授课教师将要求学生先在讨论区发帖提问，如果有必要再请学生来办公室讨论。
  5. 请慎重在讨论区公开张贴自己的代码，因为这样可能导致其他同学直接复制粘贴你的代码作为自己的作业提交，而进一步导致你的代码被查重系统判为互相抄袭。如果确实要粘贴代码的，请在讨论区发帖时勾选“仅课程组成员可见”。
  6. 尽早提问，我们尽量会在问题提出的24小时内给出回复，但是我们不保证一定在作业截止日期前回复。如果同学们都只在作业截止日期的前一两天提问，那么我们肯定是没法及时答疑的，由此造成作业未完成的情况需自行承担后果。
  7. 尽可能的回答他人提出的问题，要积极的与他人交流，这不仅会帮助他人解决困惑，也会整理自己的思路，同时也有助于发现自己潜意识当中没有认识到的问题以便授课教师帮助你弄清楚。
  8. 授人以鱼不如授人以渔，我们虽然鼓励大家积极的回答其他同学提出的问题，参与讨论区当中的讨论，但是一个好的回答应该能够启发别人的思考。例如对于提问“我希望能够对一个有n个元素的数组从小到大排序，请问在C++语言当中要怎么做？”，一个不好的回答是：“sort(a, a+n)”，而好的回答应该是：“标准库algorithm中有一个sort函数，它不仅可以实现简单的排序，还可以按照你定义的大小关系对一般对象进行排序。这个函数一般接受两个参数，是要排序容器的两个用于标注界限的迭代器，也可以接受第三个参数明确排序方式。你可以参考https://cplusplus.com/reference/algorithm/sort/来学习该函数的具体用法”。
  9. 所有问题都可以提问。不要觉得自己的问题很初级，提问了会让老师和同学觉得自己怎么这么简单的问题都不会，如果你有这个想法，你可以在讨论区发起匿名提问，这样一来就不会有人知道问题是谁提出的了！

关于课程内合作与学业诚信的特别规定

  1. 课程资料的讨论原则：在过去的教学实践中，授课教师认为学习课程资料的最佳方式是互相讨论课程资料的内容。因此课程鼓励大家通过线上（组织交流群、在课程平台讨论区发帖等）、线下（学习小组、答疑时间）等方式讨论学习课程资料，但是讨论的过程中不应当直接给出用于课程评分的作业答案，同时学生在学习过程中不得直接参考和讨论以往学期发布的任何用于课程评分的作业答案。也就是说，涉及到用于课程评分的部分必须是学生独立完成的成果。学生若实在无法想出作业的解决思路，正确的方法是通过邮件、课程平台、或者在答疑时间联系授课教师，寻求帮助。
  2. 考试纪律：课程中的所有考试均为闭卷考试，学生在考试过程中的行为应当符合《北京交通大学考试管理规定》中的各项要求。
  3. 问：使用ChatGPT等人工智能工具来参与作业书写是否违反本特别规定？答：是。
  4. 违反本特别规定的后果：学生违反本特别规定的，若是针对于课程作业的不诚信行为，该项作业成绩记为0分。若是违反考试纪律的，课程总评成绩记为0分，并视情节轻重寻求纪律处分。