Shoufeng's Blog

Graph Representation Graph Interface Graph是Undirected的（15122定义），也就是说对于vertex A和B，BA和AB是一条edge。我们将graph表示成一个data structure，其中vertex定义为无符号整数。那么一个基本的graph interface可以如下所示： 123456789101112131415161718192021222324252627282930313233343536typedef unsigned int vertex;typedef struct graph_header *graph_t;graph_t graph_new(unsigned int numvert);//@ensures \result != NULL;void graph_free(graph_t G);//@requires G != NULL;unsigned int graph_size(graph_t G);//@requires G != NULL;bool graph_hasedge(graph_t G, ...

Libraries Overview 通过使用库（libraries），程序可以复用已经编写好的代码，包括系统代码、过去编写的简单代码以及他人编写的复杂代码。库有助于隐藏不必要的细节，使代码更易于管理，并允许透明的改进。 Structure of a library: 接口（Interface）：列出了库导出的功能及其使用方法。 实现（Implementation）：实现接口中列出的功能的代码。 文档（Documentation）：解释库中功能的作用。 在编写应用程序代码时，开发者能且只能使用接口中列出的功能，不依赖于实现。编译应用程序时，需要包含库的实现。库包含系统库作为编程语言的一部分，如C0的输入输出函数，和用户定义库**：由用户编写或从互联网下载，必须与应用程序一起编译。 就15122而言，库最重要的帮助是定义了新数据类型及其使用方法。通过接口定义类型和操作，使得实现可以透明地更改，而不影响使用该类型的应用程序。 Example of Self-Sorting Arrays, SSA SSA是一个示例数据结构，类似于字符串数组，但具有报告长度的功能，并保证其元素是排序的。 ...

Strategy 3.1.5 (Proving two functions are equal) Given functions f,g:X→Yf, g: X \to Yf,g:X→Y with the same domain and codomain, in order to prove that f=gf=gf=g, it suffices to prove that f(x)=g(x)f(x)=g(x)f(x)=g(x) for all x∈Xx \in Xx∈X. Strategy 3.1.27 (Proving set identities using characteristic functions) In order to prove that two subsets U and V of a set X are eq ual, it suffices to prove that χU=χV\chi_{U} = \chi_{V}χU​=χV​. Strategy 3.2.2 (Proving a function is injective) In ord ...

Strategy 1.1.7 (Proving conjunctions) A proof of the proposition p∧qp \wedge qp∧q can be obtained by tying together two proofs, one being a proof that p is true and one being a proof that q is true. Strategy 1.1.9 (Assuming conjunctions) If an assumption in a proof has the form p∧qp \wedge qp∧q, then we may assume p and assume q in the proof. Strategy 1.1.13 (Proving disjunctions) In order to prove a proposition of the form p∨qp \vee qp∨q, it suffices to prove just one of p or q. Strateg ...

Propositional Logic Definition 0.1: Proposition is a statement to which it is possible to assign a truth value. A proposition is an umbrella term which can be used for any result. A theorem is a key result which is particularly important. A lemma is a result which is proved for the purpose of being used in the proof of a theorem. A corollary is a result which follows from a theorem without much additional effort. Sets and Numbers Definition 0.3: A set is a collection of objects. The objects i ...

本篇总结CMU 15122第一单元Deliberate Programming的全部内容（除了Contracts部分）。这门课的整体脉络还是较为清晰的，虽然大部分东西并不陌生，但从safety和correctness的角度重新审视一遍也是不错的。 Integers 涉及进制转换的内容略过不提。 Two’s Complement Two’s Complement是C0中表示数字的一种方法。C0中的整数一共占据32个比特位，其中最高的比特位是该比特位代表的负的2的31次方，也就是说，C0中的最大正整数可以用0x7FFFFFFF表示，正数的范围是0x00000000-0x7FFFFFFF(0 231−10~2^{31}-10 231−1)。当最大正整数int_max()再继续做加法的时候整数就会溢出到负数的范围内，也就是0x80000000-0xFFFFFFFF。其中0x80000000是int_min()，其顺序与正数表示相反。由此，c0能够表示的整个整数范围是[−231,231)[-2^{31}, 2^{31})[−231,231)。 对于int的操作类型有：Addition, mult ...

CMU15122开头部分讲的内容都是关于如何编写Contracts来保证程序的正确性和安全性，以及利用Contract对程序进行验证。本文简单梳理其中引出的概念。 Contract c0中有四种Contract： 1234- //@requires exp; checked before function execution- //@ensures exp; checked function returns- //@assert exp; checked wherever it is- //@loop_invariant exp; checked before the loop guard 其中@requires旨在检查函数的precondition是否满足，@ensures旨在检查postcondition是否满足。其中@ensures中可以使用\result来表示函数返回值。@loop_invariant通常检查的是循环中几个变量构成的常量表达式，其在每轮iteration检查循环条件是否满足时被检查，并且只能在循环开头写。@assert即在程序任意位置检查附上表达式的真假。 Pr ...

0 “告白的本质就是不可能告白。如果作为创作者的‘我’在作品中出现，那么就会有一个写‘作者’的‘作者’，就不能保证表现的纯粹性，从而导致告白的形式崩塌，对‘我’来说，假面是带着皮肉的表面，带着这样皮肉的假面所作的告白，不可能是真诚的告白。人终究是无法作出真正的告白的。但是极少数的情况下，只有深深嵌入了肉体之中的假面才能做到这一点。” ————三岛由纪夫 1 “深怕自己本非美玉，故而不敢加以刻苦琢磨，却又半信自己是块美玉，故又不肯庸庸碌碌，与瓦砾为伍。于是我渐渐地脱离凡尘，疏远世人，结果便是一任愤懑与羞恨日益助长内心那怯弱的自尊心。” 我是极厌恶自己的，并且平等地厌恶精神与肉体。不断站在本体的对立面，带着嘲弄地进行自我否定。是将灵魂分割成两半，一半留在躯体内敏感地捕捉着毛细血管的舒张所产生的微妙情绪，另一半却站在精神的彼岸冷眼相待，分析并时刻警惕着自己体内的那一半灵魂因天性的敏感而极易产生的得胜感。认定着这种肉体所产生的灵魂即是自身的首要敌人，且其间具有不可调和的矛盾。一者穷其一生追求纯粹的、甚至不可能的美与崇高，一者则用异常理性的眼光洞察自身，一针见血地否定前者的美。肉体所诞生的灵魂无 ...

6.1.1 Critical Sources System sources include computer harware, software, trained personnel and suppotring infrastructure. And Operating System is usually responsible for the resources management. Primary memory stores all processed data and instructions and all resulting data. It is directly connected to the processor and feed the processor with required data during the Machine Instruction Cycle. RAM and Cache memory RAM can be overwritten. And there are two types of RAM: static RAM and dyna ...

一门水课，所以直接整理大纲中要求学生掌握的问题的答案。 1.1 Environmental History Significant historical influences on the development of the environmental movement have come from literature, the media, major environmental disasters, international agreements and technological developments. (a minimum of 3 in-depth examples). Montreal Protocol: The Montreal Protocol on Substances that Deplete the Ozone Layer is the landmark multilateral environmental agreement that regulates the production and consumption of nearly 100 m ...