Virtualization is a great tool for testing/learning codes on different environment. My personal experience with virtual machine started by vmware for studying linux. At that time wsl (windows sublinu...
Graph RepresentationGraph InterfaceGraph是Undirected的（15122定义），也就是说对于vertex A和B，BA和AB是一条edge。我们将graph表示成一个data structure，其中vertex定义为无符号整数。那么一个基本的graph interface可以如下所示：1234567891011121314151617181920212...
LibrariesOverview通过使用库（libraries），程序可以复用已经编写好的代码，包括系统代码、过去编写的简单代码以及他人编写的复杂代码。库有助于隐藏不必要的细节，使代码更易于管理，并允许透明的改进。 Structure of a library: 接口（Interface）：列出了库导出的功能及其使用方法。 实现（Implementation）：实现接口中列出的功能的代码。 ...
Strategy 3.1.5 (Proving two functions are equal)Given functions $f, g: X \to Y$ with the same domain and codomain, in order to prove that $f=g$, it suffices to prove that $f(x)=g(x)$ for all $x \in X...
Strategy 1.1.7 (Proving conjunctions)A proof of the proposition $p \wedge 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. Str...
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 r...
本篇总结CMU 15122第一单元Deliberate Programming的全部内容（除了Contracts部分）。这门课的整体脉络还是较为清晰的，虽然大部分东西并不陌生，但从safety和correctness的角度重新审视一遍也是不错的。 Integers涉及进制转换的内容略过不提。 Two’s ComplementTwo’s Complement是C0中表示数字的一种方法。C0中的整数一...
CMU15122开头部分讲的内容都是关于如何编写Contracts来保证程序的正确性和安全性，以及利用Contract对程序进行验证。本文简单梳理其中引出的概念。 Contractc0中有四种Contract： 1234- //@requires exp; checked before function execution- //@ensures exp; checked function ret...
0“告白的本质就是不可能告白。如果作为创作者的‘我’在作品中出现，那么就会有一个写‘作者’的‘作者’，就不能保证表现的纯粹性，从而导致告白的形式崩塌，对‘我’来说，假面是带着皮肉的表面，带着这样皮肉的假面所作的告白，不可能是真诚的告白。人终究是无法作出真正的告白的。但是极少数的情况下，只有深深嵌入了肉体之中的假面才能做到这一点。”————三岛由纪夫 1“深怕自己本非美玉，故而不敢加以刻苦琢磨，却又...
6.1.1 Critical SourcesSystem sources include computer harware, software, trained personnel and suppotring infrastructure. And Operating System is usually responsible for the resources management. Prim...