1. Propositions 命题

2.1 Propositional Connectives 命题连接词

2.2 Variables 变量

2.3 Sets

2.3.1 Set Operations

2.4 Predicates

2.5 Quantification 量化

2.6 Relations

2.6.1 What Is A Relation?

2.6.2 Relations as Sets

2.6.3 Binary Relations as Pictures

2.6.4 Relation Example

2.6.5 Functions

2.6.6 Total vs Partial Functions 全函数 VS 部分函数

2.6.7 Relation Operations

2.6.8 Relation Joins

3. TEMPORAL LOGIC 时序逻辑

3.1 Next State

3.1.1 Transitions and Traces

3.2 Temporal Operators 时间运算符

4. SPECIFICATIONS SAY “WHAT” DESIGNS SAY “HOW”

4.1 Specifying Software

4.2 Aside: Functions as Relations

4.3 Modelling Data Types

4.4 Sequences as Relations 作为关系的序列

4.5 Searching

4.6 Pre and Postconditions 前置条件和后置条件

4.7 Formal Model-Based Specs

4.8 Advantages

4.9 Effect on Cost

4.10 Disadvantages

4.11 Difficulty

5. SPECIFICATIONS IN ALLOY

5.1 Alloy

6. LASTPASS DEMO

6.1 Alloy Modelling Overview

1. Propositions 命题

定义：A statement that is either true or false

2.1 Propositional Connectives 命题连接词

2.2 Variables 变量

Variables allow propositions to talk about state

Variables talk about different parts of the state of the formal model. (not state of the system/program)

2.3 Sets

A collection of things

2.3.1 Set Operations

2.4 Predicates

Extend propositions with the ability to quantify the values of a variable that a proposition is true for

all: Proposition P(x) holds for all values of x

all x | P[x]

all city | Raining[city]

all city: AustralianCities | Raining[city]

some: Proposition P(x) holds for at least one value of x

some x | P[x]

some city | not Raining[city]

2.5 Quantification 量化

De Morgan’s Laws

all x | P[x] is equivalent to not some x | not P[x]

some x | P[x] is equivalent to not all x | not P[x]

Alloy Specific Quantifiers

one x | P[x] P(x) holds for exactly one value x

lone x | P[x] P(x) holds for at most one value x

none x | P[x] P(x) holds for no value x

2.6 Relations

A proposition that relates things together =, <, etc.

arity: the number of things the relation relates =, < etc. are all binary relations; relate two numbers 3 < 4, (5 - 1) = (3 + 1), etc.

A relation that relates three things together: IsSum(x,y,z) <=> z = x + y

Relations are just predicate

2.6.1 What Is A Relation?

How would you write down unambiguously what a relation means?

Simplest answer: just list all of the things it relates together.

Any relation is a simply a set of tuples.

2.6.2 Relations as Sets

Factor(x,y,z) — {(x,y,z) | x = y * z}

{(1,1,1), (2,1,2), (2,2,1), (3,1,3), (3,3,1),(4,4,1), (4,2,2),…}

Use Factor to define when a number is prime, i.e. define the predicate IsPrime[x] 使用Factor来定义一个数字何时是质数，即定义谓词IsPrime[x]。

all y,z | (x,y,z) in Factor implies y = 1 or z = 1

A relation with arity n (i.e. an n-ary relation) R, is a set of n-tuples of atoms. 一个有n个算数的关系（即n-ary关系）R，是一个由n个原子图元组成的集合。

A binary (2-ary) relation R(a,b) is a set of: pairs

A ternary (3-ary) relation R(a,b,c) is a set of: triples

A unary (1-ary) relation R(a) is a set of: atoms

Sets are relations, and relations are sets. 集合是关系，而关系是集合。

Sets are predicates, and predicates are sets. 集合是谓词，而谓词是集合。

Relations are predicates, and predicates are relations. 关系是谓词，而谓词是关系。

2.6.3 Binary Relations as Pictures

2.6.4 Relation Example

Imagine 2 sets of atoms:

Username = {n1, n2, …}

Password = {p1, p2, …}

Imagine an LDAP username/password database.

LDAPDB : Username -> Password

LDAPDB ⊆

高完整性系统工程（三）： Logic Intro Formal Specification相关推荐

高完整性系统工程（一）：Intro Safety
制作满足用途的大型软件的方法 Criteria(标准) Security 安全性 Correctness 正确性 Performance 绩效 Reliability 可靠性 Usability 可用 ...
高完整性系统（4）Formal Logic （形式逻辑和 Alloy 简介）
文章目录 Story so far 形式逻辑命题 proposition 谓词 predicate 连接词 Variables Set 集合 Set operation 集合操作 Set Relat ...
高完整性系统工程（四）： Checking Formal Specifications
目录 1. Alloy Modelling Overview 2. 有限状态机(Finite State Machines) 3. 在Alloy中建模有限状态机(Modelling FSMs in A ...
高完整性系统工程（十一）：Fault Tolerant Design
目录 1. INTRODUCTION TO FAULT TOLERANCE 1.2 Definitions 1.3 Two Kinds of Faults 1.4 Hardware vs Softwa ...
高完整性系统工程（九）：Invariants
目录 1. INVARIANTS 1.1 例子 1.2 正式的证明 1. INVARIANTS 一个不变式需要满足以下三个属性: 当循环开始时,不变式是正确的在每一次循环迭代之后,不变式仍然是正确的 ...
高完整性系统工程（一）： Safety Engineering, HAZOP Fault Tree Analysis
目录 1. 因果性不等同于相关性 2. HAZOP 2.1 学习HAZOP 2.2 HAZOP概览 2.3 Assessing Hazard Risks 评估 2.4 示例场景 2.5 HAZOP G ...
高完整性系统 (2)：Requirement 与 Design 阶段的风险控制——Hazards, HAZOP, Fault Tree
文章目录安全性工程流程 Hazards 反事实推理(CounterFactual Reasoning) 案例1 案例2 案例3 HAZOP: HAZARDS AND OPERABILITY STUD ...
聊聊高并发（三十六）Java内存模型那些事（四）理解Happens-before规则
在前几篇将Java内存模型的那些事基本上把这个域底层的概念都解释清楚了,聊聊高并发(三十五)Java内存模型那些事(三)理解内存屏障这篇分析了在X86平台下,volatile,synchronize ...
深度学习（14）TensorFlow高阶操作三: 张量排序
深度学习(14)TensorFlow高阶操作三: 张量排序一. Sort, argsort 1. 一维Tensor 2. 多维Tensor 二. Top_k 三. Top-k accuracy(To ...

高完整性系统工程（三）： Logic Intro Formal Specification

1. Propositions 命题

2.1 Propositional Connectives 命题连接词

2.2 Variables 变量

2.3 Sets

2.3.1 Set Operations

2.4 Predicates

2.5 Quantification 量化

2.6 Relations

2.6.1 What Is A Relation?

2.6.2 Relations as Sets

2.6.3 Binary Relations as Pictures

2.6.4 Relation Example

高完整性系统工程（三）： Logic Intro Formal Specification相关推荐

最新文章

热门文章