CMU 15-122

这是CMU 15-122的笔记. 老实说, 若不是有人气到我了, 说我完全不懂计算机, 那我可能五六年之后 (现在是2024年) 才会学习它. 这个课程的名字是Principles of Imperative Computation, 即命令式计算原理, 实际上就是教如何在C语言中进行编程的课程, 但却是按照编程语言学家所认为的正确方式教授. 从一开始学生就需要学习如何对于命令式程序进行推理.

最开始学生使用一门叫做C0的编程语言进行编程, 大致上它可以算是C语言的一个精心设计的安全子集, 有着良定义的句法和语义. 之后, 学生从C0过渡到真正的C语言. 课程的内容大致上是计算机科学常识, 基本的(命令式)编程常识, 以及(命令式)算法和数据结构.

当然, 在上这门课之前, 还是要把C0语言先安装好. 课程提供了deb格式的安装包.

讲座1

这节课比较简单, 但主要是为了说明基本的风格. 其检视了一个函数的定义, 似乎是一个施行幂运算的函数. 然而, 也有一点小问题. 之后, 引入了循环不变量, 前条件, 后条件来对于程序进行推理, 并最终证明了修改之后的程序的正确性. C0语言支持用某种形式来表达循环不变量, 前条件, 后条件, 其他的断言等内容. 并可进行执行程序时的动态检查. 一方面, 它可以供人阅读. 另一方面, 它也可供机器执行. 当然, 有些东西不可能在其中表达, 比如说终止性. 这必须另外说明并证明. 本课的最后, 还提示了一下关于模算术的一点内容, 即该函数的正确性是在模算术意义下的.

讲座2

讲座2是关于整数的表示的. 首先, 介绍了自然数的二进制表示, 以及进制的转换. 鉴于将二进制表示转换为整数值其实就是多项式求值, 所以介绍了Horner规则, 中国人也将其称为秦九韶算法. 将一个自然数值转换为二进制表示当然就是通过不断做带余除法. 在C0语言中, int的值用32bit来表示, 其实就是two's complement表示的带符号整数, 所以是模232的算术, 取值范围是从2312311. 两个这样的表示相加其实就是小学的竖式加法, 当然实际机器不是这么实现的. 经过简单的思考可知, 加逆 (也就是相反数) 可以是bitwise complement再加上一: x=~x+1. 并且, 1的表示不论是多少位的版本, 都会是全为1的串. 十六进制表示的话, 不论C0还是C在词法上前面都会加上0x. 210=1K. 220=1M. 230=1G. 240=1T.

除法或许是要特别注意的, 不像加法或乘法即便当成无符号数计算也是一样. 鉴于2的大于1的幂次都不是素数, 所以非零元不一定都有逆, 于是我们考虑带余除法. 我们用x/y表示整数除法, x%y表示整数模 (modulus) 运算, 其中y0. 我们希望它们满足(x/y)y+(x%y)=x.当然, 这还不足以刻画两种运算. 另外, 我们希望0|x%y|<|y|. 不过, 在y不整除x的情况下, 这仍然留下了modulus是正是负的不确定性, 所以需要进一步的规定来限制. 一种方式是约定整数除法运算永远向着零的方向截断. 这会导致一个现象, 就是在x为负的情况下整数模运算的结果永远都是负的, 而x为正的情况下整数模运算的结果永远都是正的. 另一种约定是整数除法永远向下取整. 这会导致整数模运算的正负和y的正负是一致的. C0语言使用第一种约定.

我们不仅用整数来进行数字运算, 很多时候整数也用来表示其他种类的数据, 因此所谓的按位运算也是很有用的. 按位与: &. 按位或: |. 按位非: ~. 按位不可兼或 (异或): ^. 除了按位运算, 左移和右移也是常见的运算. x << k代表x左移k位, x >> k代表x右移动k位. 鉴于C0的(带符号)整数是32bit的, 所以0k<32. 左移的时候, 空出来的位填0, 这相当于乘2k. 右移的时候, 空出来的位填充最高位, 此即所谓算术右移. 这样做之后, 首先我们看出来x将保持符号. 其次, 它相当于除以2k, 向下取整. (这个可以通过计算证明.)

作为一个位的例子, 整数可以用来表示颜色. 这是所谓的ARGB表示. 用3个8bit分别表示RGB, 还剩8bit表示不透明度, 顺序就是ARGB. 如果p表示颜色, 那么(p >> 16) & 0xFF可以用来获得红色分量的值. 这其实就是把红色分量移到最右边的位置, 然后用掩码给其他位都填0. 反过来, 如果想修改某个分量的值, 比如绿色, 设g包含了我们所想修改到的值, 那么(p & 0xFFFF00FF) | (g << 8)就是我们所想要的答案.

讲座3

讲座3是关于array的.