哈夫曼编码 Huffman Codes   广泛使用的数据压缩技术   假设数据是一个字符序列   寻找存储数据的有效方法   想法：   –使用字符出现的频率来建立表示每个字符的最佳方式   二进制字符代码  –用二进制字符串唯一地表示一个字符 定长码 Fixed-Length Codes 例如：包含100000个字符的数据文件    需要3位   a=000，b=001，c=010，d=011，e=100，f=101   需要：100000·3=300000位   可变长度码 Variable-Length Codes 例如：包含100000个字符的数据文件    将短码字分配给频繁字符，...

本章介绍了几个额外的证明策略和策略，使我们能够开始证明函数程序更有趣的属性。 我们将看到：  如何在“向前”和“向后”证明中使用辅助引理； 如何对数据构造函数进行推理——特别是如何利用它们是内射的和不相交的事实； 如何强化归纳假设，以及何时需要强化；和 关于如何通过案例分析进行推理的更多详细信息。  应用策略 The apply Tactic 我们经常遇到这样的情况，即需要证明的目标与上下文中的某个假设或之前证明的引理完全相同。 Theorem silly1 : forall (n m : nat), n = m -> n = m. Proof. intros n m eq. //在这里...

附加练习 Additional Exercises 57: 2 stars, standard (fold_length) 列表上的许多常见功能可以按折叠方式实现。例如，以下是长度的替代定义： Definition fold_length {X : Type} (l : list X) : nat := fold (fun _ n => S n) l 0. Example test_fold_length1 : fold_length [4;7;0] = 3. Proof. reflexivity. Qed.  证明折叠长度的正确性。（提示：了解自反性比siml更积极地简化表达式可能会有...

作为数据的函数 Functions as Data 与大多数现代编程语言一样——特别是其他“函数”语言，包括OCaml、Haskell、Racket、Scala、Clojure等——Coq将函数视为一级公民，允许它们作为参数传递给其他函数、作为结果返回、存储在数据结构中等。 高阶函数 Higher-Order Functions 操纵其他函数的函数通常称为高阶函数。这里有一个简单的例子： Definition doit3times {X : Type} (f : X->X) (n : X) : X := f (f (f n)).  这里的参数f本身就是一个函数（从X到X）；doit3ti...

谓词逻辑的语义 Semantics of Predicate Logic 谓词逻辑 Predicate Logic 谓词逻辑的语义 Semantics of predicate logic  模型 Models 语义蕴涵 Semantic entailment 平等的语义学 Semantics of equality 谓词逻辑的不可判定性 Undecidability of predicate logic  谓词逻辑公式的真值 Truth Values for Predicate Logic Formulas 在命题逻辑中，给出了公式  我们可以根据给定的估值（p和q的假设真值）给它一个真值（...

Examples Tutorial Third /* -*- Mode:C++; c-file-style:"gnu"; indent-tabs-mode:nil; -*- */ /* * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as * published by the Free Software Foundation; * * This program is dis...

Examples Tutorial Second /* -*- Mode:C++; c-file-style:"gnu"; indent-tabs-mode:nil; -*- */ /* * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as * published by the Free Software Foundation; * * This program is di...

Examples Tutorial First /* -*- Mode:C++; c-file-style:"gnu"; indent-tabs-mode:nil; -*- */ /* * This program is free software; you can redistribute it and/or modify * it under the terms of the GNU General Public License version 2 as * published by the Free Software Foundation; * * This program is dis...

要求 利用网络仿真工具NS3实现一种改进的安全路由协议(自主选择)，要求：  设置仿真空间1*1 KM2 随机生成100个对等节点（趋向于均匀分布） 通信协议任选（如使用Zigbee 协议框架） 最大传输速率200kb/s，最大通信距离75m，源节点与目标节点间距1KM以上。 （选1）该路由协议可抗冲突，考虑遮挡模型（可穿透与不可穿透）、丢包、中间辅助节点中途损坏，可考虑多路径（至少考虑一种环境，此部分10分） （选1）计算总丢包率（需给出丢包率计算公式，提示每个点实际收包数/理论收包数） 数据量1MB，协作传输，并尽可能的提高传输效率 （选2）结合上题安全路由技术，设计无线传感器网络数据安全...

要求 Wireshark无线抓包实验  下载并安全装Wireshark 要求抓取明文用户名和口令  获取WPA用户口令  提示：字典攻击(aircrack)

Chap 10 环与理想 - 理想   10.5 理想和商环     10.5.1 理想  定义 10.5.1 左理想 右理想 理想 例 10.5.1 平凡理想 定理 10.5.1 定理 10.5.2 多个理想的交集 定义 10.5.2 X生成的（左）理想 生成元 有限生成的 主理想 定理 10.5.3 < X >中元素的显示表示 主理想环 定理 10.5.4 理想的运算 和理想 积理想 定理 10.5.5 定理 10.5.6    10.5.2 商环  定理 10.5.7 商环R/Ⅰ的构造 商环    10.5.3 环同态分解定理  定理 10.5.8 同态分解定理 自然同态 定...

在本章中，我们将介绍加密哈希函数并探讨它们的一些应用。在最基本的层次上，哈希函数提供了一种将长输入字符串映射到短输出字符串（有时称为摘要）的方法。主要要求是避免冲突，或避免映射到同一摘要的两个输入。抗冲突散列函数有多种用途。我们将在这里看到的一个示例是另一种标准化为HMAC的方法，用于实现消息身份验证代码的域扩展。 除此之外，散列函数在密码学中已变得无处不在，它们通常用于要求比抗冲突性强得多的属性的场景。将加密散列函数建模为“完全不可预测”（也称为随机预言）已变得很常见，我们将在本章后面详细讨论该框架以及围绕该框架的争议。在这里，我们只涉及随机oracle模型的几个应用程序，但当我们转到公钥加...

4.1 消息完整性 Message Integrity 4.6  考虑以下MAC长度为l（n）＝2n-2的消息的使用伪随机函数F：输入消息 （其中） 和键，算法Mac输出。算法Vrfy是以自然的方式定义的，（Gen，Mac，Vrfy）安全吗？证明你的答案。 参考答案 4.6  4.7  设F为伪随机函数。显示以下每个MAC都是不安全的，即使用于验证固定长度的消息。 （在每种情况下，Gen输出一个统一的 。设 表示整数i的n/2位编码。） （a） 要验证消息，，计算 参考答案 4.7  4.25  设F是强伪随机置换，并定义以下固定长度加密方案：在输入消息和键，算法Enc选择一个一致的并计算 。...

多态性 Polymorphism 在本章中，我们将继续发展函数式编程的基本概念。关键的新思想是多态性（将函数抽象为它们所操作的数据类型）和高阶函数（将函数视为数据）。我们从多态性开始。 多态列表 Polymorphic Lists 在上一章中，我们一直在处理只包含数字的列表。显然，有趣的程序还需要能够使用其他类型的元素操作列表——布尔列表、列表列表等等。我们可以为每种类型定义一个新的归纳数据类型，例如。。。 Inductive boollist Inductive boollist : Type := | bool_nil | bool_cons (b : bool) (l : boollis...