高完整性系统工程(八):Hoare Logic

这篇具有很好参考价值的文章主要介绍了高完整性系统工程(八):Hoare Logic。希望对大家有所帮助。如果存在错误或未考虑完全的地方,请大家不吝赐教,您也可以点击"举报违法"按钮提交疑问。

目录

1. 霍尔逻辑(Proving Programs Correct)

1.1 警告(Caveats)

1.2 误解(Misconception)

1.3 编程语言(Programming Language)

1.4 程序(Programs)

1.5 证明(Proof)

1.6 霍尔三元组(Hoare Triples)

1.7 逻辑(Logic Refresher)

1.8 推理规则(Inference Rules)

1.9 赋值语句(Assignment Statements)

1.10 赋值规则(Rule of Assignment)

1.11 推论规则(Rule of Consequence)

1.12 结合两个规则(Combining the Two Rules)

2. 赋值规则与最弱前置条件规则 Assignment Rule as Weakest Precondition Rules

2.1 最弱前置条件推理 Weakest Precondition Reasoning

2.2 序列规则 Rule of Sequencing

2.3 Larger Programs

2.3.1 逐步推理

2.3.2 最终证明

2.4 Skip

2.5 条件规则 Conditional Rule

2.5.1 示例:寻找最大值

2.6 迭代规则

2.6.1 迭代的例子:计算阶乘


1. 霍尔逻辑(Proving Programs Correct)

霍尔逻辑是一种理论方法,用于证明程序的正确性,即程序的运行结果符合我们预期的功能和效果。但是,证明程序的正确性并不意味着程序就一定没有错误或bug,还存在一些潜在的问题和误解:

1.1 警告(Caveats)

  • 如果证明了程序的正确性,就保证没有错误吗?答案是不确定的,原因如下:
    • 错误的规格说明(Incorrect specification):你可能证明了错误的事情。
    • 程序与已证明内容不同(Program differs from what was proved):证明总是基于数学模型,而实际的程序可能与模型存在差异。
    • 程序执行与理想状态不同(Program's execution differs from ideal):可能由于编译器或硬件错误,硬件故障等导致。

1.2 误解(Misconception)

  • 证明过程很困难吗?如果你仔细理解编程,证明过程并不困难。

1.3 编程语言(Programming Language)

这部分介绍了如何在霍尔逻辑中表示程序的基本元素。

  • 程序(Procedures)

    • P := procedure p(v1,...,vn) ^= S
    • 其中v1, . . .,vn是变量名,p是程序名,S是程序语句。
  • 表达式(Expressions)

    • E := NE | a[NE]
    • NE := n | v | E1+E2 | E1-E2 | E1xE2 | E1/E2 | etc...
    • 这里,n是一个数字,v是一个变量,a是一个数组变量,NE是一个数字表达式,E是一个表达式。
  • 布尔表达式(Booleans)

    • B := true | false | 反B | E1=E2 | E1 <= E2 | etc. . .
    • B代表布尔表达式。
  • 语句(Statements)

    • S := skip | v:=E | a[NE] := E | p(E1,...,En) | S1;S2 | if B then S1 else S2 endif | while B do C done
    • 这里,v是一个变量,a是一个数组变量,p是一个程序名。S代表语句。

通过这些基本元素和结构,我们可以在霍尔逻辑中建立和证明程序的模型。

1.4 程序(Programs)

这部分示例展示了一个阶乘程序FACTORIAL,输入是n,输出是f。主程序调用了FACTORIAL (10,f)

procedure p1 (v1,...,vm) ^= S1
...
procedure pn (v1,...,vn) ^= Sn
S -> “main” program: -> FACTORIAL (10,f)

procedure FACTORIAL(in n, out f)
    f := 1
    i := 0
    while i /= n do
        i:=i+1
        f:=f×i
    end while
end procedure

FACTORIAL (10,f)

1.5 证明(Proof)

证明程序的正确性是遵循程序的结构,自顶向下。为了证明关于X的某件事,我们需要分析X的内部组件。

1.6 霍尔三元组(Hoare Triples)

霍尔逻辑使用霍尔三元组 {P} S {Q} 来描述程序的行为,其中:

  • P 是前置条件(Precondition);
  • S 是程序;
  • Q 是后置条件(Postcondition)。

例如,{ x = 2 } x := x + 1 { } 描述的是,在执行 x := x + 1 之前,x 的值是 2。这是最强后置条件的示例。另一个示例是最弱前置条件 { } x := x + 1 { x = 1 },这表示在 x := x + 1 执行后,x 的值应该是 1

1.7 逻辑(Logic Refresher)

这部分是对逻辑符号的一些基本介绍:

  • A → B 表示“蕴含”,即如果 A 为真,则 B 也为真;
  • ¬A 表示“非”或“否定”,表示 A 不为真;
  • A ∧ B 表示“与”或“合取”,表示 AB 都为真;
  • A ∨ B 表示“或”或“析取”,表示 AB 至少有一个为真;
  • true 表示永远为真的命题;
  • false 表示永远为假的命题。

1.8 推理规则(Inference Rules)

推理规则用于逻辑推理。以下是一些示例:

  • 模态三段论(Modus Ponens):如果 A 为真,并且 A → B 为真,则 B 为真;

高完整性系统工程(八):Hoare Logic

  • 公理(Axiom): true 总是为真;

高完整性系统工程(八):Hoare Logic

  • 结构规则(Structural Rule):如果 AB 都为真,则 A ∧ B 为真。

高完整性系统工程(八):Hoare Logic

1.9 赋值语句(Assignment Statements)

赋值语句是最基本的程序语句。霍尔逻辑为赋值语句提供了一种形式化的表示方法,该表示方法包含前置条件、赋值语句本身和后置条件。例如:

  • { x = 2 } x := x + 1 { } 表示在执行 x := x + 1 之前,x 的值是 2
  • { } x := x + 1 { x = 1 } 表示在 x := x + 1 执行后,x 的值是 1

1.10 赋值规则(Rule of Assignment)

赋值规则描述了在给变量 x 赋值表达式 E 后,前置条件 P 如何变为后置条件。规则为:

高完整性系统工程(八):Hoare Logic

  • ( ) / {P[E/x]} x := E {P}

例如,为了证明 { } x := x + 1 { x = 1 },我们需要找到满足 {P[E/x]} x := E {P}P。在这个例子中,Px = 1Ex + 1,所以 P[E/x]x + 1 = 1,也就是 x = 0。所以,我们有 { x = 0 } x := x + 1 { x = 1 }

1.11 推论规则(Rule of Consequence)

推论规则描述了如何通过已知的霍尔三元组 {P}S{Q} 得到新的霍尔三元组 {P'}S{Q'}。规则为:

高完整性系统工程(八):Hoare Logic

  • (p' => P, Q => Q', {P}S{Q}) / ({P'}S{Q'})

例如,假设我们已经证明了 { x = 0 } x := x + 1 { x = 1 },那么我们可以通过推论规则得到 { x = 0 } x := x + 1 { x > 0 },因为 x = 1 蕴含 x > 0

1.12 结合两个规则(Combining the Two Rules)

这部分展示了如何将赋值规则和推论规则结合起来使用。首先,使用推论规则来扩大前置条件,然后使用赋值规则。这是一个通用的模式。例如,假设我们希望证明 { x = 0 } x := x + 1 { x > 0 },我们可以先应用推论规则,然后再应用赋值规则:

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic

  • (x = 0 → ?P { ?P } x := x + 1 { x > 0 }) / ({ x = 0 } x := x + 1 { x > 0 })

高完整性系统工程(八):Hoare Logic

  • ( ( ) / (x = 0 → x + 1 > 0) ( ) / ({ x + 1 > 0 } x := x + 1 { x > 0 }) ) / ({ x = 0 } x := x + 1 { x > 0 })

此模式的推导过程说明了在程序验证中,推论规则和赋值规则是如何配合使用的。

2. 赋值规则与最弱前置条件规则 Assignment Rule as Weakest Precondition Rules

  • { } x := E {P}

这个规则描述了给定某个具体后置条件P时,如何计算保证P之后成立的最弱前置条件。如果我们有一个形如x := E的赋值语句,并且我们知道执行这个赋值语句之后必须满足某个条件P,那么我们可以通过计算最弱前置条件来确定在执行这个赋值语句之前必须满足的条件。对于其他类型的语句(例如if, while, skip, sequencing等),我们将看到同样形式的规则,这使得我们可以从一个具体的后置条件计算最弱前置条件。

2.1 最弱前置条件推理 Weakest Precondition Reasoning

给定具体的前置条件P'和Q以及一些程序S,要证明:

  • {P′} S {Q}

首先应用后果规则来概括前提条件,给出两个要证明的目标:

  • {?P} S {Q}

然后,通过应用最弱前置条件规则来计算?P是什么

  • P′ ⟹ ?P

一旦计算出?P,最后检查此蕴含关系是否成立。

这个过程描述了给定具体的前置条件P'和后置条件Q以及一些程序S时,如何证明形如{P′} S {Q}的命题。首先,我们应用 consequence rule 来将前置条件泛化,这给出了我们需要证明的两个目标:{?P} S {Q}P′ ⟹ ?P。然后,我们通过应用最弱前置条件规则计算出 ?P 是什么。一旦 ?P 被计算出来,最后检查这个蕴含关系是否成立。

2.2 序列规则 Rule of Sequencing

序列规则描述了如何通过两个霍尔三元组 {P} S1 {R}{R} S2 {Q} 推导出新的霍尔三元组 {P} S1; S2 {Q}

  • ({P} S1 {R}, {R} S2 {Q}) / {P} S1; S2 {Q}

例如,为了证明 {x = 0} x := x+1; x := x+1 {x=2},我们可以先应用后果规则,然后应用序列规则和赋值规则。最后我们需要检查 x = 0 → x+2=2 是否成立,这就是最弱前置条件推理。

高完整性系统工程(八):Hoare Logic

Proof:

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic高完整性系统工程(八):Hoare Logic

2.3 Larger Programs

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic

高完整性系统工程(八):Hoare Logic

如何使用之前讨论过的规则(后果规则,序列规则和赋值规则)来推理有关更大程序的性质。考虑下面的程序,它将x和y的值交换:

{x = X ∧ y = Y} 
t := x;
x := y; 
y := t
{x = Y ∧ y = X}

我们将这个要证明的性质写成形式化的形式:{x = X ∧ y = Y} t := x; x := y; y := t {x = Y ∧ y = X}

要使用序列规则推理此程序,我们需要考虑程序中每个赋值语句的前置条件和后置条件。

2.3.1 逐步推理

推理过程从程序的最后一步开始(这是因为后置条件与最后一步最直接相关),然后反向工作到程序的开始。每个步骤都有一个前置条件?P和一个后置条件?R。

首先,我们将原始的程序拆分为三个更简单的步骤:t := x;x := y;y := t;。然后,我们为每个步骤计算其最弱前置条件,这些最弱前置条件就是在执行每个步骤之前必须满足的条件。计算过程使用了之前提到的赋值规则:{P[E/x]} x := E {P},其中 P[E/x] 表示将 P 中的 x 替换为 E

例如,第一步的后置条件是{x = Y ∧ y = X},通过赋值规则我们可以计算其最弱前置条件为{x = Y ∧ t = X}。这意味着在执行 y := t 之前,我们需要确保 x 的值是 Yt 的值是 X

首先关注的是最后的部分
 {?R2}
y := t
{x = Y ∧ y = X}
根据{P[E/x]} x := E {P}变成:
{(x = Y ∧ y = X) [t/y]}
y := t
{x = Y ∧ y = X}
变成:
{x = Y ∧ t= X}
y := t
{x = Y ∧ y = X}

然后我们会将这个新计算的前置条件作为下一步(x := y)的后置条件,再次应用赋值规则,计算其最弱前置条件为{y = Y ∧ t = X}。

接下来是证明
{?R1}
x := y;
{x = Y ∧ t= X}
推导:
{(x = Y ∧ t = X) [y/x]}
x := y;
{x = Y ∧ t= X}
变成:
{y = Y ∧ t = X}
x := y;
{x = Y ∧ t= X}

我们继续这个过程,将{y = Y ∧ t = X}作为下一步(t := x)的后置条件,再次应用赋值规则,计算其最弱前置条件为{y = Y ∧ x = X}。

接下来到了:
{?P}
t := x;
{y = Y ∧ t = X}
推导:
{(x = Y ∧ t = X) [x/t]}
t := x;
{y = Y ∧ t = X}
变成:
{y = Y ∧ x = X}
t := x;
{y = Y ∧ t = X}

2.3.2 最终证明

最后,我们需要检查初始的前置条件{x = X ∧ y = Y}是否蕴含最初计算的前置条件{y = Y ∧ x = X}。在这个例子中,这是正确的,因为它们都表达了相同的事实(只是顺序不同)。所以,我们成功地证明了这个程序的性质:它将x和y的值交换。换句话说:
在最后一步,我们使用了逻辑等价性,即 x = X ∧ y = Y 是等价于 y = Y ∧ x = X 的,这意味着如果 x = Xy = Y 都为真,那么 y = Yx = X 也都为真,反之亦然。因此,我们证明了 {x = X ∧ y = Y} t := x; x := y; y := t {x = Y ∧ y = X} 是正确的。

2.4 Skip

高完整性系统工程(八):Hoare Logic

skip 是一个在程序中不执行任何操作的语句。在 Hoare 逻辑中,我们可以写作 {P} skip {P},这意味着在任何条件 P 下执行 skip,结束后的条件依然是 P。因为 skip 并不改变任何变量的值,所以前后的条件保持一致。

2.5 条件规则 Conditional Rule

高完整性系统工程(八):Hoare Logic

条件语句的形式化规则可以写作 {P1} S1 {Q}, {P2} S2 {Q} / {(B => P1) ∧ (¬B => P2)} if B then S1 else S2 endif {Q}。这个规则表明,在执行 if 语句之前的条件应当是当条件 B 成立时 P1 成立,当条件 B 不成立时 P2 成立。然后分别对 S1S2 应用对应的前提条件 P1P2,在两种情况下的后置条件都是 Q

换句话说,给定后置条件Q,如果我们知道在B为真的情况下执行S1可以达到Q,并且在B为假的情况下执行S2也可以达到Q,那么整个if语句在前置条件为B蕴含P1并且非B蕴含P2的情况下可以保证Q。

2.5.1 示例:寻找最大值

考虑这样一个简单的程序,它的目的是使得r等于x和y中的最大值:

{true}
if x > y then
r := x;
else
r := y;
endif
{r ≥ x ∧ r ≥ y}

首先,对于 if 语句的两个分支,我们分别计算最弱前提条件。

Apply consequence rule first (p' => P, Q => Q', {P}S{Q}) / ({P'}S{Q'})
{	}
if x > y then
r := x;
else
r := y;
endif
{r ≥ x ∧ r ≥ y}
({P1} S1 {Q}, {P2} S2 {Q}) / ({(B => P1) ∧ (¬B => P2)} if B then S1 else S2 endif {Q})
{true}
{?P}
if x > y then
r := x;
else
r := y;
endif
{r ≥ x ∧ r ≥ y}
( ) / ({P[E/x]} x := E{P})
{true}
{(x>y → ?P1) ∧ (x≤y → ?P2)}
if x > y then
{?P1}
r := x;
{r ≥ x ∧ r ≥ y}
else
{?P2}
r := y;
{r ≥ x ∧ r ≥ y}
endif
{r ≥ x ∧ r ≥ y}
{true}
{(x>y → x ≥ x ∧ x ≥ y) ∧ (x≤y → y ≥ x ∧ y ≥ y)}
if x > y then
{x ≥ x ∧ x ≥ y}
r := x;
{r ≥ x ∧ r ≥ y}
else
{y ≥ x ∧ y ≥ y} 
r := y;
{r ≥ x ∧ r ≥ y}
endif
{r ≥ x ∧ r ≥ y}
{true}
{(x>y → x ≥ x ∧ x ≥ y) ∧ (x≤y → y ≥ x ∧ y ≥ y)}
if x > y then
{x ≥ x ∧ x ≥ y}
r := x;
{r ≥ x ∧ r ≥ y}
else
{y ≥ x ∧ y ≥ y} 
r := y;
{r ≥ x ∧ r ≥ y}
endif
{r ≥ x ∧ r ≥ y}

r := x; 的最弱前提条件是 x ≥ x ∧ x ≥ y

r := y; 的最弱前提条件是 y ≥ x ∧ y ≥ y

所以,整个 if 语句的最弱前提条件是 (x > y → x ≥ x ∧ x ≥ y) ∧ (x ≤ y → y ≥ x ∧ y ≥ y)。这个条件是一个逻辑表达式,表示 x 大于 y 时,x 应该大于等于 xy,而当 x 小于等于 y 时,y 应该大于等于 xy

在得到每个分支的最弱前提条件之后,我们只需要验证这个前提条件是满足的,就能证明整个程序的正确性。

在这个例子中,前提条件 (x > y → x ≥ x ∧ x ≥ y) ∧ (x ≤ y → y ≥ x ∧ y ≥ y) 是满足的,因为对于任意的 xyx 总是大于等于 xy 总是大于等于 y,所以无论 xy 的大小关系如何,r 的值总是大于等于 xy

所以,我们成功证明了 {true} if x > y then r := x; else r := y; endif {r ≥ x ∧ r ≥ y} 是正确的。

2.6 迭代规则

高完整性系统工程(八):Hoare Logic

迭代规则是用于处理 while 循环语句的形式化规则。规则为:({P ∧ B} S {P} P ∧ ¬B => Q) / ({P} while B do S done {Q})

这里的

  • P 代表循环不变量(loop invariant)。
  • B 是循环条件,
  • S 是循环体。
  • Q 是我们希望在循环结束后达成的后置条件。

这个规则表示的是,在每次循环开始时,如果循环条件 B 成立,且循环不变量 P 满足,那么在执行完循环体 S 后,循环不变量 P 仍然保持。如果循环条件 B 不成立,那么 P 必须能推出我们期望的后置条件 Q

2.6.1 迭代的例子:计算阶乘

接下来是一个例子,程序如下,其目标是计算N的阶乘并将结果存储在n中:

{true}
i := 0;
n := 1;
while i ≠ N do
i := i + 1 
n := i * n;
done
{	}
{true}
{?Q}
i := 0;
{?P}
n := 1;
{?I}
while i ≠ N do
i := i + 1 
n := i * n;
done
{n = N!}
{true}
i := 0;
n := 1;
while i ≠ N do
i := i + 1;
n := i * n;
done
{n = N!}

我们希望在循环结束后,n 的值等于 N!,即 N 的阶乘。在此过程中,我们尝试找到一个适合的循环不变量 P,使得我们能够应用迭代规则来证明这个程序的正确性。

首先,我们假设循环不变量 In = i!,表示在每次循环开始时,n 的值等于 i 的阶乘。

然后我们需要检查在执行循环体之后,这个循环不变量是否仍然保持。

{?I}
while i ≠ N do
i := i + 1 
n := i * n;
done
{n = N!}

这里的P是我们假设的循环不变量 {?I},B是循环条件i ≠ N,Q是{n = N!}

根据({P ∧ B} S {P} P ∧ ¬B => Q) / ({P} while B do S done {Q})

{?I} -- P
while i ≠ N do
{?I ∧ i ≠ N} -- 这里是P∧B
i := i + 1
n := i * n;
{?I} -- P
done
{n = N!} -- B

高完整性系统工程(八):Hoare Logic

?I ∧ i = N -> n = N!
Let ?I be: n = i!
{n = i!}
while i ≠ N do
{n = i! ∧ i ≠ N} 
i := i + 1
n := i * n;
{n = i!}
done
{n = N!}
n = i! ∧ i = N → n = N!

i := i + 1 执行之后,我们需要 n = (i+1)!。由于下一步是 n := i * n,我们希望能够在此步之前满足 (i+1)*n = (i+1)!。通过替换前面的循环不变量,我们可以得到 i*n = i!。这表示,在执行 n := i * n 之后,n 的值应该等于 (i+1)!,这也是我们希望的结果。

{n = i! ∧ i ≠ N}
i := i + 1
n := i * n;
{n = i!}
{n = i! ∧ i ≠ N}
{?R2}
i := i + 1 
n := i * n;
{n = i!}

赋值规则  ( ) / ({P[E/x]} x := E {P})

{n = i! ∧ i ≠ N}
{?R2}
i := i + 1
{?R}
n := i * n;
{n = i!}
{n = i! ∧ i ≠ N}
{?R2}
i := i + 1
{(n = i!)[i * n / n]} 
n := i * n;
{n = i!}

首先,我们考虑的是n := i * n; 对于这个表达式我们使用赋值规则。这里的P是 n = i!,x是n := i * n,{?R}是将P中的n换成i * n,即{(n = i!)[i * n / n]} ,意思为在n = i!中,使用i * n替换掉n。

{n = i! ∧ i ≠ N}
{?R2}
i := i + 1
{i*n = i!}
n := i * n;
{n = i!}

其次,我们考虑 i := i + 1 这个语句,我们希望找到一个 R2 ,使得 {n = i! ∧ i ≠ N} i := i + 1 {R2} 成立。根据赋值规则,我们找到 R2 = (n = i!)[i+1/i],也就是(i+1)*n = (i+1)!。

{n = i! ∧ i ≠ N}
{(i*n = i!)[i+1/i]}
i := i + 1
{i*n = i!}
n := i * n;
{n = i!}
{n = i! ∧ i ≠ N}
{(i+1)*n = (i+1)!}
i := i + 1
{i*n = i!}
n := i * n;
{n = i!}

然后,我们需要证明 n = i! ∧ i ≠ N → (i+1)*n = (i+1)! 成立,也就是说,如果当前 n 等于 i 的阶乘,且 i 不等于 N,那么 (i+1)*n 一定等于 (i+1)!。这个式子在数学上是成立的,因为 (i+1)*n 在这里等于 (i+1)*i!,而 (i+1)*i! 正好等于 (i+1)!

n = i! ∧ i ≠ N -> ((i+1)*n = (i+1)!)

这里的赋值规则指的是 Hoare 逻辑中的赋值规则,形式如下:

( ) / ({P[E/x]} x := E {P})

这个规则是说,如果在赋值语句 x := E 之后,程序的状态满足某个条件 P,那么在执行赋值语句之前,程序的状态必须满足把 E 代入 xP。换句话说,我们可以把 P 中所有的 x 替换为 E,得到赋值语句前的条件 P[E/x]

最后,我们需要确认当循环条件不成立时,即 i ≠ N 为假,也就是 i = N 时,循环不变量 n = i! 能够推出后置条件 n = N!。显然这个条件是满足的。

经过以上的推理,我们证明了这个程序是正确的,即这个程序能够计算 N!。在程序结束时,n 的值等于 N!

这个过程是用 Hoare 逻辑进行程序正确性证明的典型例子,显示了如何找到合适的循环不变量,以及如何通过形式化的推理规则进行程序的正确性证明。

{true}
{?Q}
i := 0;
{?P}
n := 1;
{n = i!}
while i ≠ N do
 {n = i! ∧ i ≠ N}
 {(i+1)*n = (i+1)!}
 i := i + 1
 {i*n = i!}
 n := i * n;
 {n = i!}
done
{n = N!}

还是因为赋值表达式,{?P} 就是 {(n = i!)[1/n]}

{true}
{?Q}
i := 0;
{(n = i!)[1/n]}
n := 1;
{n = i!}
while i ≠ N do
 {n = i! ∧ i ≠ N}
 {(i+1)*n = (i+1)!}
 i := i + 1
 {i*n = i!}
 n := i * n;
 {n = i!}
done
{n = N!}
{true}
{?Q}
i := 0;
{1 = i!}
n := 1;
{n = i!}
while i ≠ N do
 {n = i! ∧ i ≠ N}
 {(i+1)*n = (i+1)!}
 i := i + 1
 {i*n = i!}
 n := i * n;
 {n = i!}
done
{n = N!}

同理,因为赋值表达式,{?Q} 就是 {(1 = i!)[0/i]}

{true}
{(1 = i!)[0/i]}
i := 0;
{1 = i!}
n := 1;
{n = i!}
while i ≠ N do
 {n = i! ∧ i ≠ N}
 {(i+1)*n = (i+1)!}
 i := i + 1
 {i*n = i!}
 n := i * n;
 {n = i!}
done
{n = N!}
{true}
{1 = 0!}
i := 0;
{1 = i!}
n := 1;
{n = i!}
while i ≠ N do
 {n = i! ∧ i ≠ N}
 {(i+1)*n = (i+1)!}
 i := i + 1
 {i*n = i!}
 n := i * n;
 {n = i!}
done
{n = N!}
Does true -> 1 = 0! ? YES!

完成!文章来源地址https://www.toymoban.com/news/detail-473122.html

到了这里,关于高完整性系统工程(八):Hoare Logic的文章就介绍完了。如果您还想了解更多内容,请在右上角搜索TOY模板网以前的文章或继续浏览下面的相关文章,希望大家以后多多支持TOY模板网!

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处: 如若内容造成侵权/违法违规/事实不符,请点击违法举报进行投诉反馈,一经查实,立即删除!

领支付宝红包 赞助服务器费用

相关文章

  • 数据库系统概论—安全、完整性

    数据库的安全性指保护数据库以防 不合法 使用所造成的数据泄露、更改或破坏 2.1用户身份鉴别 静态口令鉴别 动态口令鉴别 生物鉴别特征 智能卡鉴别 2.2存取控制 自主存取控制:给用户限权(DAC,C1级) 强制存取控制:给数据库对象一定的密级(MAC,B1级) 2.3自主存取控制方法(授

    2024年02月03日
    浏览(50)
  • 物理安全对工控系统数据完整性的影响如何评估和管理?

    随着工业自动化和数字化程度的不断提高, 工业控制系统的数据安全性和完整性日益受到重视. 工业控制系统 (ICS) 是指那些应用于制造、交通和其他领域的关键基础设施的计算机系统和网络设备. 这些系统通常涉及大量敏感信息如工艺参数和历史记录等的数据交换与存储. 因此

    2024年02月21日
    浏览(36)
  • 如何关闭苹果系统完整性保护SIP(System Integrity Protection)

    您需要进入 Mac 的恢复模式(Recovery Mode)。请按照以下步骤操作: 关闭您的 Mac。 按下电源按钮,然后立即按住 Command 和 R 键。持续按住这两个键,直到您看到 Apple 徽标或地球图标出现在屏幕上。 当您进入恢复模式后,会看到 macOS 实用工具窗口。从菜单栏中选择“实用工具

    2024年02月15日
    浏览(40)
  • 数据库系统头歌实验八 数据库完整性、安全设计

    第1关:执行 CREATE USER 创建以2022100904为用户名的用户,同时设置其密码为root1234 第2关:给予创建的用户2022100904在mydata数据库中授予\\\"J\\\" 表 SELECT 权限(注意创建权限时的用户名为\\\'用户名\\\'@\\\'localhost\\\'),不允许转授此权限给其它用户。 第3关:给予创建的用户2022100904、2022100908在

    2024年02月05日
    浏览(103)
  • 信号完整性(SI)电源完整性(PI)学习笔记(一)信号完整性分析概论

    信号完整性分析概论 1.信号完整性(SI):指在高速产品中由互联线引起的所有问题;研究当互联线与数字信号的电压电流波形相互作用时,其电气特性如何影响产品的性能,SI又叫信号波形失真。 2.电源完整性(PI):指为有源器件供电的互联线及各相关元件上的噪声;PDN(

    2024年02月04日
    浏览(52)
  • 信号完整性与电源完整性分析-Eric Bogatin

    第一章 信号完整性概论 1-任何一段互联,无论线长和形状,也无论信号的上升边如何,都是一个由信号路径和返回路径构成的传输线。信号在互联前进的每一步,都会感受到瞬时阻抗。若阻抗恒为常量,信号质量就会优良 2-信号网络不仅包括信号路径,还包括信号电流的返回

    2024年02月06日
    浏览(58)
  • Mysql列的完整性约束(调整列的完整性约束)

    目录 一、 主键PK、外键FK和 唯一键UK 新增 删除         修改         修改默认值DEFAULT、自增长和非空NK 总结 alter table [table_name] add constraint [constraint_name] [unique key| primary key|foreign key] ([column_name])         1.通过如下命令查询键值的约束名:                 

    2024年02月01日
    浏览(54)
  • mysql索引--普通索引,唯一索引,主键索引,参照完整性约束,数据完整性约束

    -- 方法1:create index -- 对employee表的员工部门号列创建普通索引depart_ind -- create index depart_ind on employees(员工部门号); -- 对employee表的姓名和地址列创建复合索引ad_ind; -- create index ad_ind on employees(姓名,地址); -- 对departments表的部门名称列创建唯一索引un_ind; -- create unique index un_ind

    2023年04月21日
    浏览(45)
  • 5.1 实体完整性

    第5章 数据库完整性笔记 定义 : 完整性 :确保数据的正确性和相容性。 正确性 :数据与现实世界语义相符、反映实际状况。 相容性 :同一对象在数据库的不同关系表中数据逻辑上是一致的。 示例 : 学号唯一性。 性别限定为男或女。 本科学生年龄为14-50之间的整数。 学

    2024年02月06日
    浏览(45)
  • 2.4数据完整性验证

    1.数据完整性概述 数据完整性指数据不会被非授权更改或破坏,如篡改、删除、插入等 主要类型:带恢复的连接完整性、不带恢复的连接完整性、选择字段连接完整性、无连接完整性、选择字段无连接完整性 主要实现技术:基于密码技术的完整性保护和基于非密码技术的完

    2024年02月08日
    浏览(55)

觉得文章有用就打赏一下文章作者

支付宝扫一扫打赏

博客赞助

微信扫一扫打赏

请作者喝杯咖啡吧~博客赞助

支付宝扫一扫领取红包,优惠每天领

二维码1

领取红包

二维码2

领红包