程序语言与编译原理

上课自由度：本来还能喘口气的课后作业现在原地转生成了小测，自由度为0，自由度直接躺平交白卷 考核标准：这每节课小测是要顶替作业的生态位了吗，因为ai起飞所以不布置作业改埋伏小测吗，本来是保平时分的东西现在毕业变身成催命符了，小测还挺正式，电脑手机一律收走，然而我亲眼看见前排有人拿手机偷偷搜，考的东西给的做题时间短到你怀疑人生基本做不完，所以是不是要偷摸举着手机凹搜索才保得住平时分啊，我不想平时分当场核爆，或许这锅得算我头上吧......

课程内容： 上课自由度： 考核标准： 授课质量： 求求了教务，把这门课改成选修课吧，真的听不懂曹大师讲的coq，我感觉自己是在用肉体接航天发射密码。

2026年1月23日：出成绩更新 曹大师发功了，期末成绩直接开根乘10，一通操作猛如虎，最后总成绩居然还过得去。 所以加一颗星，嘿嘿。 不过我那coq小测实在拉得离谱（35/100），平时分照样被扣了5分，薅我一撮羊毛。 --- 2026年1月7日：考试结束更新 这卷子和往年卷子简直不是一个物种啊？总共七道题，就两道题会做，剩下好几道看都看不懂……尤其是不动点定理居然能和活性分析叠一起出一道证明题？？？这是碳基生物能想出来的题目吗。还有这个assume是啥？复习的时候压根没翻到过。第一题NFA一脸人畜无害，真下手了根本写不出来，啊啊啊。 上考场半小时，一道题都没做出来，然后曹大师一直在我旁边晃来晃去，还盯着我解答看，我当时真的当场心态爆炸。 我嘞个豆。 我来逐题点评一下： - 第一题：写出 NFA 对应的正则表达式。 - 点评：看着像只乖猫，结果这 NFA 和上课举例的那些简单结构完全不是一个路子，它有两条互相交叉、纠缠的路线，构造直接卡死当场。 - 第二题：写一个上下文无关语法，来规定 `&&` 和 `||` 以及 `!` 的先后顺序，并且这里的 `&&` 和 `||` 之间是同一优先级的。然后做一个移入规约分析。 - 点评：这道题还是能做的。 - 第三题：在 SimpleWhile 中引入 break，然后试着定义这一情况下程序的指称语义。 - 点评：看不懂，不知道怎么入手。 - 第四题：结合活性分析与不动点定理的知识，构造一个函数，说明活性分析的结果是这个函数的最小不动点。 - 点评：最难读懂题目意思的一题，题干看着就很复杂。证明“不动点”是容易的，但证明“最小”这一步，我不太会。 - 第五题：在 SimpleWhile 中引入非确定性赋值，判定此时的 while 语句的指称语义的 inf 集合是否是某个函数的不动点。 - 点评：还是不知道要干嘛，感觉上是伪命题，但不知道怎么说。 - 第六题：写出集合单子中 assume 和 bind 的定义，并证明 assume-bind 推理的正确性。 - 点评：啥是 assume？复习时根本没看…… - 第七题：定义一个 swap 函数（交换两个内存中数据的位置），写出符号执行过程以说明其正确性。 - 点评：最像人类的一题，非常简单。 --- 2025年11月26日 19点40分： 我觉得这 coq 语言太傻逼了，又要求每一步都必须完全正确，不能出错，结果自己又搞一堆省略写法，或者搞一些另外的符号，美其名曰语法糖，其实这糖是鹤顶红味儿的，要把我毒死了。 无语了…… --- 课有点难，而且老师讲得有点抽象，不太好学，尤其是coq出现之后，真是一头雾水。 等我后面继续更新。 --- coq小测，180分的题目，我拿了35分，哈哈哈🤡🤡🤡🤡 我还准备了一晚上+一上午…… 带着你的coq一边去吧。 小测占总成绩10分，哈哈哈，牛逼了哥们😭😭😭 --- 这coq是人学的？我感觉自己也不算笨，但上到后面根本听不懂，看代码都费劲，还搞coq证明，合适吗？我提议这门课改成选修…… ---- 12-31更新： 复习时才感觉到，曹大师的讲义真是言简意赅，现在整理笔记，有种为《春秋》作传的感觉。哎哎，曹大师什么时候能照顾一下我们这些笨蛋，把讲义写得详细一点啊。

课程内容：coq 上课自由度：低 授课质量：还行，但是coq这玩意儿以后基本查无此人啊。我绞尽脑汁也想不到这辈子什么时候还得跟coq再续前缘。 课程workload大到离谱，我就纳了闷了，大三花大量时间跟coq死磕到底图个啥，是图它证明不了我的人生吗。

课程内容：编译原理含量少得像方便面里的牛肉粒，coq证明含量多得像不要钱的白开水。 上课自由度：还行，人少到一定地步就挨个点名，中途来也行。课上会提问，但你爱干啥干啥——反正也听不懂。 考核标准：平时作业35+出勤5+期末30+编程作业10+理论作业20。 授课质量：没上过的尽管来一起喷，不必划走。 1. 授课内容，大伙都以为是来学编译原理的，结果拐进了程序语言，满屏coq证明。请问c老师，学程序正确性证明对我未来有一丁点帮助吗？为啥把你的科研直接扣学生头上？这是纯纯浪费我们时间，对您又有什么好处？？ 2. 考核标准，上一届学长的大作业是编程作业理论作业二选一，但据说难度差得肉眼可见（这谁看不出来啊）。于是天才的c老师本学期抛出天才构想：**大家都要做理论作业和编程作业**，这不就公平了吗？*nmlgb*一个学期两个大作业加期末考试，大作业里还塞着超绝coq证明，这是碳基生物想出来的？？ 3. 大作业选题，文档写的是先来后到分配，但c老师给隔壁组分编程作业时开始随机乱发。**理论作业选题时一点任务详情都不给**，你只拿到一个题目，难度全靠自己猜，分配好像也不是先来后到，还有一个组邮件直接石沉大海。 4. 大作业难度，隔壁组据我所知好像1800行证完level3，而我们组几个level难度毫无区分，难度曲线是高原，**光算法定义就甩了400+行代码让我们自己啃，里面甚至还有bug**。**小组最终证明代码近10000行，换来理论作业50%左右的分数**。请问c老师出题时到底有没有考虑题目难度不一样？还是您压根不知道这题什么难度？选题的时候都不知道要证啥，难度全看抽盲盒。跟c老师交流下来的观感就是：他随手编了几道题，写个算法一丢，具体怎么证我怀疑他自己都不知道。 + 顺嘴提一句，最后好像是4/6个组做完了证明，但我不觉得是我们组能力有问题，我自己确实没怎么搞明白，但我的义父们绝对不比别的组笨或懒，我觉得我们组的任务就是比别的组难。我也不认为cqx本人能在短时间内证完这个命题。另外，我们**大作业里用到的某处定义十五周才开始讲，十六周周五才讲完**，诗人我吃。 5. 答疑，包括但不限于：，"老师请问我们这个方向能证通吗""你们自己证试试，能通就能通，不能通就不能通"；"我们没证过题目，给出的定义可能有问题，是因为你们开始证明太晚，没及时发现"；"请问老师定义是不是错了""自己判断是不是错了，你们觉得错了自己改过来就行"。 6. 期末，最后两题单子和分离逻辑，单子感觉跟上课讲的形式完全不沾边，分离逻辑丢你一段单链表c代码，让你自己写类似sllseg的东西。上届学长说特别简单，可能像c老师这种天才根本不知道我这种普通人的智商水平，随手加点难度就把我干懵了（我还以为我单子学得特透彻，ohno）。 7. 平时作业满分三分向下取整，放最后是因为这是槽点里最微不足道的一个。 本门课是我在交大上过体验最差的一门，如上所述，每个环节都揣着一个放到别的课能被冲烂的槽点，而伟大的c老师愣是集齐了一整套。哥们除了这门课核心学积分94+，这门课还是我花时间最多的一门，80出头的分数比我通识课都低。写coq大作业时只有深深的无力感，因为完全不知道到底咋做。 悲伤的是后面还会有一届届ieee cs的同学来坐这个大牢，再想想ieee cs的保研卷度（指硕士夏令营初筛卡小专业50%），ieee cs就是交大最烂cs，且看不到任何好转的希望。 本来是想骂人的，但把槽点列一遍已经耗尽我所有力气。 sb东西，nt课程 **Admitted.**