Virtualization is a great tool for testing/learning codes on different environment. My personal experience with virtual...
Graph RepresentationGraph InterfaceGraph是Undirected的（15122定义），也就是说对于vertex A和B，BA和AB是一条edge。我们将graph表示成一个data structure，...
LibrariesOverview通过使用库（libraries），程序可以复用已经编写好的代码，包括系统代码、过去编写的简单代码以及他人编写的复杂代码。库有助于隐藏不必要的细节，使代码更易于管理，并允许透明的改进。 Structure o...
Strategy 3.1.5 (Proving two functions are equal)Given functions $f, g: X \to Y$ with the same domain and codomain, in o...
Strategy 1.1.7 (Proving conjunctions)A proof of the proposition $p \wedge q$ can be obtained by tying together two proo...
Propositional Logic Definition 0.1: Proposition is a statement to which it is possible to assign a truth value. A propos...
本篇总结CMU 15122第一单元Deliberate Programming的全部内容（除了Contracts部分）。这门课的整体脉络还是较为清晰的，虽然大部分东西并不陌生，但从safety和correctness的角度重新审视一遍也是不...
CMU15122开头部分讲的内容都是关于如何编写Contracts来保证程序的正确性和安全性，以及利用Contract对程序进行验证。本文简单梳理其中引出的概念。 Contractc0中有四种Contract： 1234- //@requi...
0“告白的本质就是不可能告白。如果作为创作者的‘我’在作品中出现，那么就会有一个写‘作者’的‘作者’，就不能保证表现的纯粹性，从而导致告白的形式崩塌，对‘我’来说，假面是带着皮肉的表面，带着这样皮肉的假面所作的告白，不可能是真诚的告白。人终...
6.1.1 Critical SourcesSystem sources include computer harware, software, trained personnel and suppotring infrastructure...