DraonAbyss

分类

C++(3) CodeForces(23) LeetCode(3) 函数语言程序设计(40) 安全编程(1) 密码学基础(17) 无线网络安全(5) 笔记(16) 算法设计与分析(22) 编译原理与技术(16) 网络安全数学基础(3) 计算机逻辑基础(8) 题解(37)

/ 注册

TA的专栏 167篇文章 11人订阅

【题解】SQL 入门

36篇文章 18251人学习

【学习】函数语言程序设计

39篇文章 1641人学习

【学习】密码学基础

16篇文章 1083人学习

【学习】算法设计与分析

22篇文章 1924人学习

【学习】无线网络安全

6篇文章 2960人学习

计算机逻辑基础

4篇文章 1462人学习

【学习】网络安全数学

7篇文章 882人学习

12篇文章 551人学习

2篇文章 542人学习

23篇文章 1665人学习

全部文章（共194篇）

INDPROP.归纳定义命题.案例研究：正则表达式来自专栏

Case Study: Regular Expressions ev属性提供了一个简单的例子来说明归纳定义和对其进行推理的基本技术，但它并不十分令人兴奋——毕竟，它相当于我们已经看到的两个非归纳均匀度定义，并且似乎没有提供任何具体的好处。为了更好地理解归纳定义的威力，我们现在展示如何使用它们来模拟...

2021-12-20

0 524

INDPROP.归纳定义命题.归纳关系来自专栏

Inductive Relations 一个由数字（如ev）参数化的命题可以被认为是一个属性——也就是说，它定义了nat的子集，即命题可证明的那些数字。同样，一个双参数命题可以被认为是一种关系——也就是说，它定义了一组可证明命题的对。

2021-12-20

0 438

INDPROP.归纳定义命题.在证明中使用证据来自专栏

Using Evidence in Proofs 除了构建数字是偶数的证据外，我们还可以破坏这些证据，这相当于对如何构建数字的推理。引入带有归纳声明的ev不仅告诉Coq构造函数ev_0和ev_SS是证明某个数字是ev的有效方法，而且这两个构造函数是证明数字是ev的唯一方法。换句话说，如果有人给我...

2021-12-20

0 691

INDPROP.归纳定义命题.归纳定义命题来自专栏

INDPROP INDUCTIVELY DEFINED PROPOSITIONS 归纳定义命题 Set Warnings "-notation-overridden,-parsing,-deprecated-hint-without-locality". From LF Require Export...

2021-12-20

0 658

IMP.简单命令式程序.Coq自动化来自专栏

Coq Automation 最后一个证明中重复的次数有点烦人。如果算术表达式的语言或被证明合理的优化明显更复杂，那么它将开始成为一个真正的问题。到目前为止，我们所做的所有证明都只使用了Coq的一小部分策略，而完全忽略了它自动构造部分证明的强大功能。本节将介绍其中的一些设施，我们将在接下来的几章中...

2021-12-19

0 712

IMP.简单命令式程序.算术和布尔表达式来自专栏

在本章中，我们将更认真地研究如何使用Coq来研究其他东西。我们的案例研究是一种简单的命令式编程语言Imp，它体现了传统主流语言（如C和Java）的一个微小核心片段。这是一个用Imp编写的熟悉的数学函数。 Z := X; Y := 1; while ~(Z = 0) do ...

2021-12-19

0 1020

第24.1章单源最短路径·Bellman-Ford算法来自专栏

Patrick教授希望找到一条从菲尼克斯(Phoenix)到印第安纳波利斯(Indianapolis)的最短路径。给定一幅美国的道路交通图，上面标有所有相邻城市之间的距离，Patrick教授怎样才能找出这样一条最短的路径呢? 一种可能的办法当然是，先将从菲尼克斯到印第安纳波利斯的所有路径都找出来，将...

2021-12-18

0 791

第25.1章所有结点对的最短路径问题.最短路径和矩阵乘法来自专栏

25.1 最短路径和矩阵乘法

2021-12-18

0 423

第22.3章基本的图算法.深度优先搜索来自专栏

22.3 深度优先搜索深度优先搜索所使用的策略就像其名字所隐含的:只要可能，就在图中尽量“深入”。深度优先搜索总是对最近才发现的结点v的出发边进行探索，直到该结点的所有出发边都被发现为止。一旦结点v的所有出发边都被发现，搜索则“回溯”到v的前驱结点(v是经过该结点才被发现的)，来搜索该前驱结点的出...

2021-12-17

0 734

第22.2章基本的图算法.广度优先搜索来自专栏

22.2 广度优先搜索广度优先搜索发现前驱父节点 BFS(G,s) for each vertx u ∈ G.V - {s} u.color = WHITE u.d = ∞ u.Π = NIL s.color = GRAY s.d = 0 s.Π = NIL Q ...

2021-12-17

0 507