历史匿名回执 ·
课程内容：程序分析=龙书后半本的压缩包，数据流、控制流一顿咔咔。ppt直接空运国外教授（http://infolab.stanford.edu/~ullman/dragon/w06/w06.html ）。然后软件测试泡个面，SAT和SMT撒点料。ppt也是国际航班直达。程序验证先来点概念漱漱口，接着Alloy和UML，最后微软的Sepc#登场。ppt继续拿来主义（https://santos.cs.ksu.edu/771-Distribution/syllabus.html ）。 上课自由度：高，签到？不存在的。 考核标准：9次平时作业，写代码和书面双拼，每次权重一样。 讲课质量：老师语速慢得能孵蛋，看直播简直是专注力火葬场，回放2.5倍速还嫌它慢。ppt基本是把国外教授“十多年前”的老古董Ctrl+C，然后删掉作者名穿上新马甲。 几次作业质量还行，比如从零手搓数据流分析、写个简单SAT Solver。不过有点散装，希望改改（也许抄抄NJU的Tai-e？）。 令人难绷的是，程序验证部分的内容年久失修。老师最后一节课说现在最流行的是Coq，那为啥不直接Coq开课，非要去盘Alloy和UML这些上古陪葬品？直接上《Software Foundations》也可以啊（ 作业给分还不错，没考试没大作业，算是温柔一刀。 更新了链接（指在链接和括号之间加入空格防止markdown把括号算入链接的一部分）