Coq学习——FRAP阅读笔记Chap3 CHAPTER 3 Data Abstraction Algebraic Interfaces for Abstract Data Types 举队列为例，在一般编程中，我们构造出数据结构就 ok 了。但是如果我们要遵照形式化正确证明，我们还要补充一个规则集合，并用 data type 的操作量化。还是讲队列，需要满足两条： \[dequeue(empty) = \cdot\] \[\fo 2020-07-09 Computer Science 形式化验证 形式化验证
Coq学习——FRAP阅读笔记Chap2 CHAPTER 2 Formalizing Program Syntax Concrete Syntax 程序定义来自程序语言，程序语言定义来自它的语法。语法描述了哪些短语是结构正确的。语义（semantics）表达了程序的意义（mean）。从concrete syntax，规定了哪些字符序列是可接受的。 举例算术运算，我们使用文法（grammar）来表述，给出 BNF，这部分理解，略过。 2020-07-09 Computer Science 形式化验证 形式化验证
Coq学习——FRAP阅读笔记Chap1 CHAPTER 1 Why Prove the Correctness of Program 传统工程学有标准的数学工具来设计工业产品。能保证产出的安全性和适用性。这些标准或多或少，在工程师设计阶段会被考虑到。由于标准从更高角度严格制定，所以根据标准进行的设计安全性是有保证的。 那为什么软件工程没有对应的公认标准，以使程序员们可以确信自己的系统是安全、可靠、正确的呢？答案是：这些概念和工具可能 2020-07-06 Computer Science 形式化验证 形式化验证
《孤独六讲》读书笔记 两版序言 早期哲学思想上的不同造成了如今“孤独”在中西方文化中含义的不同。 “西方从‘太阳’、‘唯一’发展出‘孤独’这个词，产生类似庄子哲学‘独与天地精神往来’的自负的孤独感” “汉语从儒家人际伦理的缺失发展出‘孤独’二字，总使人哀婉悲悯。” “两个不同的文化，从语文开始，赋予了‘孤独’不同的生命意涵。” 序言谈柏拉图的《飨宴篇》，现今的人类都是不完整的，在神的惩罚下，每个人都被 2020-07-02 Life 阅读 阅读 待完善
密码技术学习——Keccak论文总结 摘要部分 理论部分 已有成果研究 Keccak 自诞生以来，经历了密码学界广泛的分析，全世界各高校与机构的研究对有关 Keccak 算法（及其相关的衍生算法）的研究成果以及 Keccak 团队的密码学分析被汇总在 Team Keccak 网站中，以方便研究者们相互讨论学习。另外该网站上还长期开放着 Keccak 原像与碰撞攻击挑战赛（The Keccak Crunchy Crypto Col 2020-06-29 Computer Science 密码学 待完善 密码学 Keccak