高完整性系统工程(三): 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

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 ⊆ 𝒫 (Username x Password)

2.6.5 Functions

For every username, there is only one password in LDAPDB

all u:Username, pw1:Password, pw2:Password | LDAPDB(u,pw1) and LDAPDB(u,pw2) implies pw1 = pw2

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

LDAPDB : Username -> Password

Does every username in Username have a password?

A total function gives an answer for every (type-correct) argument

A partial function is one that is not total

2.6.7 Relation Operations

 

xQ

2.6.8 Relation Joins 

3. TEMPORAL LOGIC 时序逻辑

3.1 Next State

if x is a variable, then x’ refers to x’s value in the next state 如果x是一个变量,那么x'指的是x在下一个状态中的值

To specify that x is incremented, we would write 要指定x被递增,我们可以写成

x’ = x + 1

Predicates that talk about x are also allowed to talk about x’s value in future states, e.g. x’, x’’ etc. and how it relates to x’s current value 谈论x的谓词也被允许谈论x在未来状态下的价值,例如x',x''等,以及它与x的当前价值的关系。

These predicates define state transitions 这些谓词定义了状态转换

3.1.1 Transitions and Traces

3.2 Temporal Operators 时间运算符

We can also write predicates that talk about future and even past states using temporal operators 我们还可以使用时间运算符编写谈论未来甚至是过去状态的谓词

always P

after P

eventually P

P; Q

equivalent to P and (after Q)

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

4.1 Specifying Software

Specify modules

Formally describe (an abstraction of) the module’s state 正式描述(抽象的)模块的状态

Formally describe the behaviour of the module’s operations (e.g. procedures, functions etc.). 正式描述模块的操作行为(如程序、函数等)

Behaviour specified in terms of state (transition) relations. 用状态(转换)关系来指定行为。

Trivial example:                  a counter

State: natural number         n : ℕ

Operation: increment         n’ = n+1

4.2 Aside: Functions as Relations

4.3 Modelling Data Types 

Data types modelled as sets, relations, functions etc. 以集合、关系、函数等为模型的数据类型。

4.4 Sequences as Relations  作为关系的序列

4.5 Searching

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

Precondition: Specifies the assumptions made by a procedure/function 前提条件。指明一个程序/函数所做的假设

Postcondition: Specifies the behaviour, assuming that the precondition holds 后置条件。指定行为,假设前提条件成立

Precondition for binary search: list is sorted 二进制搜索的前提条件:列表被排序

sorted(list) <=> all i : ℤ | i < #list implies list[i] ≤ list[i+1]

4.7 Formal Model-Based Specs

Model the behaviour of each operation as a relation 将每个操作的行为建模为一种关系

The relation captures the relationship between the operation’s inputs and outputs 该关系捕捉到操作的输入和输出之间的关系

In general: relates the states before and after the operation 一般来说:将操作前后的状态联系起来

Says how they are allowed to differ (postcondition) under assumptions about the inputs (precondition) 说出了在关于输入(前提条件)的假设下允许它们有什么不同(后置条件)

Says what the operation does, not how it does it. 说的是操作做什么,而不是它如何做

4.8 Advantages

  • Small
  • Unambiguous
  • Abstract from Implementation
  • Machine-Checkable
  • Forces thinking up-front
  • Gets mistakes out of the way early (i.e. when they are cheaper to fix)
  • 小型
  • 毫不含糊
  • 从实现中抽象出来
  • 可由机器检查
  • 迫使人们提前思考
  • 尽早消除错误(即当它们的修复成本较低时)。

4.9 Effect on Cost

4.10 Disadvantages

  • Requires specialised expertise 需要专门的专业知识
  • Might lengthen time to implementation 可能会延长实施的时间
  • Loads more effort early in the development process 在开发过程的早期要付出更多的努力
  • Not necessarily well suited to projects with rapidly changing requirements. 不一定很适合于需求快速变化的项目
  • (So it’s important to get your HAZOP etc. correct) (所以,正确地进行HAZOP等是很重要的)

4.11 Difficulty

All programmers know many formal languages 所有的程序员都知道许多形式语言

Specs are shorter and thus simpler to write than code 规范更短,因此比代码更容易编写

Specs say only what not how 规范只说什么,不说怎么做

Programs must say both 程序必须说明这两点

Ordinary programmers not trained to write and read formal specs 普通程序员没有受过编写和阅读正式规范的训练

5. SPECIFICATIONS IN ALLOY

5.1 Alloy

6. LASTPASS DEMO

6.1 Alloy Modelling Overview

signatures: declaring sets and relations 声明集合和关系

facts: axioms that hold over signatures and globally constrain the model to rule out nonsense 适用于签名的公理,并在全局上约束模型以排除无意义的东西

predicates: define relations between variables in a model, used to specify operations, state transitions 定义模型中变量之间的关系,用于指定操作和状态转换

functions: shorthand for expressions 表达式的简写

本文来自互联网用户投稿,该文观点仅代表作者本人,不代表本站立场。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如若转载,请注明出处:/a/1196.html

如若内容造成侵权/违法违规/事实不符,请联系我们进行投诉反馈qq邮箱809451989@qq.com,一经查实,立即删除!

相关文章

ZYNQ硬件调试-------day2

ZYNQ硬件调试-------day2 1.ILA&#xff08;Integrated Logic Analyzer &#xff09; 监控逻辑内部信号和端口信号;可以理解为输出。可单独使用 2.VIO&#xff08;Virtual Input/Output &#xff09; 实时监控和驱动逻辑内部信号和端口信号&#xff0c;可以理解为触发输入。不可…

第十四届蓝桥杯三月真题刷题训练——第 14 天

目录 第 1 题&#xff1a;组队 题目描述 运行限制 代码&#xff1a; 第 2 题&#xff1a;不同子串 题目描述 运行限制 代码&#xff1a; 思路&#xff1a; 第 3 题&#xff1a;等差数列 题目描述 输入描述 输出描述 输入输出样例 运行限制 代码&#xff1a; 思…

Dubbo原理简介

Dubbo缺省协议采用单一长连接和NIO异步通讯&#xff0c;适合于小数据量大并发的服务调用&#xff0c;以及服务消费者机器数远大于服务提供者机器数的情况。 作为RPC&#xff1a;支持各种传输协议&#xff0c;如dubbo,hession,json,fastjson&#xff0c;底层采用mina,netty长连接…

nginx详解(概念、Linux安装、配置、应用)

1.nginx是什么 百度百科 看百度百科的解释&#xff0c;第一句话就是错的。“Nginx (engine x) 是一个高性能的HTTP和反向代理web服务器”&#xff0c;从语法来看&#xff0c;去掉形容词就是&#xff1a;Nginx是服务器&#xff0c;nginx怎么会是服务器呢&#xff0c;nginx只是一…

Matlab进阶绘图第8期—聚类/分类散点图

聚类/分类散点图是一种特殊的特征渲染散点图。 聚类/分类散点图通过一定的聚类、分类方法&#xff0c;将特征相近的离散点划分到同一个类别中&#xff0c;进而将每个离散点赋予类别标签&#xff0c;并利用不同的颜色对不同的类别进行区分。 本文使用Matlab自带的gscatter函数…

C语言变量和数据类型的使用

文章目录前言一、将变量输出打印到控制台1.整形变量的输出2.浮点型变量的输出1.flaot的输出2.doble的输出3.float和double输出的区别4.%f,%10.2f......二、数据类型的大小总结前言 上一篇文章我们学习了C语言变量和数据类型的基本概念那么今天我们就具体的来看看如何在代码中使…

css实现文字大小自适应

在页面编写中经常会碰到页面自适应的问题&#xff0c;也就是页面内部的元素会随着窗口的放大缩小而放大缩小&#xff0c;box可以通过calc 百分比的形式做到页面自适应&#xff0c;但是box内的字体却无法做到这点&#xff0c;往往box自适应大小了&#xff0c;内部的字体还是原来…

selenium(5)-------自动化测试脚本(python)

1)alert框的处理 前提:我们是不可以通过控制台直接定位元素的方式去选中这个alert框的&#xff0c;例如说xpath直接进行定位元素 1)先获得弹框的操作句柄:alertdriver.switch_to.alert 2)再次调用accept方法进行关闭弹窗:alert.accept() from selenium import webdriver import…

强化学习分类与汇总介绍

1.强化学习&#xff08;Reinforcement Learning, RL&#xff09; 强化学习把学习看作试探评价过程&#xff0c;Agent选择一个动作用于环境&#xff0c;环境接受该动作后状态发生变化&#xff0c;同时产生一个强化信号(奖或惩)反馈给Agent&#xff0c;Agent根据强化信号和环境当…

【python刷题】leecode官方提示“->“,“:“这些符号是什么意思?什么是Type Hints?

作者&#xff1a;20岁爱吃必胜客&#xff08;坤制作人&#xff09;&#xff0c;近十年开发经验, 跨域学习者&#xff0c;目前于海外某世界知名高校就读计算机相关专业。荣誉&#xff1a;阿里云博客专家认证、腾讯开发者社区优质创作者&#xff0c;在CTF省赛校赛多次取得好成绩。…

JavaSE基础总结

JDK与JRE JDK&#xff0c;全称Java Development Kit&#xff0c;Java开发工具包 JRE&#xff0c;全称Java Runntime Environment&#xff0c;Java运行环境 JDK包含后者JRE。 JDK也可以说是Java SDK&#xff08;Software Development kit&#xff0c;软件开发工具包&#xff09;…

JVM高频面试题

1、项目中什么情况下会内存溢出&#xff0c;怎么解决&#xff1f; &#xff08;1&#xff09;误用固定大小线程池导致内存溢出 Excutors.newFixedThreadPool内最大线程数是21亿(2) 误用带缓冲线程池导致内存溢出最大线程数是21亿(3)一次查询太多的数据&#xff0c;导致内存占用…

基于深度学习的农作物叶片病害检测系统(UI界面+YOLOv5+训练数据集)

摘要&#xff1a;农作物叶片病害检测系统用于智能检测常见农作物叶片病害情况&#xff0c;自动化标注、记录和保存病害位置和类型&#xff0c;辅助作物病害防治以增加产值。本文详细介绍基于YOLOv5深度学习模型的农作物叶片病害检测系统&#xff0c;在介绍算法原理的同时&#…

百度的文心一言 ,没有想像中那么差

robin 的演示 我们用 robin 的演示例子来对比一下 文心一言和 ChatGPT 的真实表现&#xff08;毕竟发布会上是录的&#xff09;。 注意&#xff0c;我使用的 GPT 版本是 4.0 文学创作 1 三体的作者是哪里人&#xff1f; 文心一言&#xff1a; ChatGPT&#xff1a; 嗯&a…

C++ STL:vector的使用方法及模拟实现

目录 一. vector概述 二. vector接口函数的使用方法和模拟实现 2.1 vector类模板的成员变量 2.2 构造函数的使用和模拟实现 2.2.1 构造函数的使用方法 2.2.2 构造函数的模拟实现 2.3 析构函数的模拟实现 2.4 赋值运算符重载函数的使用和模拟实现 2.4.1 函数的使用 2.…

MybatisPlus------MyBatisX插件:快速生成代码以及快速生成CRUD(十二)

MybatisPlus------MyBatisX插件&#xff08;十二&#xff09; MyBatisX插件是IDEA插件&#xff0c;如果想要使用它&#xff0c;那么首先需要在IDEA中进行安装。 安装插件 搜索"MyBatisX"&#xff0c;点击Install&#xff0c;之后重启IDEA即可。 插件基本用途&…

蓝桥杯嵌入式第四课--定时器

前言蓝桥杯对于定时器这部分的考察主要集中在定时器中断、PWM输出以及输入捕获三个方面&#xff0c;本节课着眼于应用&#xff0c;介绍一下定时器的使用。定时器中断一、基础概念对没接触过定时器的新手来说&#xff0c;如果想要快速上手定时器的使用&#xff0c;首先要先对定时…

Python每日一练(20230318)

目录 1. 排序链表 ★★ 2. 最长连续序列 ★★ 3. 扰乱字符串 ★★★ &#x1f31f; 每日一练刷题专栏 &#x1f31f; Golang每日一练 专栏 Python每日一练 专栏 C/C每日一练 专栏 Java每日一练 专栏 1. 排序链表 给你链表的头结点 head &#xff0c;请将其按 升序 …

卷积神经网络CNN识别MNIST数据集

这次我们将建立一个卷积神经网络&#xff0c;它可以把MNIST手写字符的识别准确率提升到99%&#xff0c;读者可能需要一些卷积神经网络的基础知识才能更好的理解本节的内容。 程序的开头是导入TensorFlow&#xff1a; import tensorflow as tf from tensorflow.examples.tutor…

C语言老题新解16-20 用命令行打印一些图案

文章目录11 打印字母C12 输出国际象棋棋盘。13 打印楼梯&#xff0c;同时在楼梯上方打印两个笑脸。14 输出9*9 口诀。15 有一道题要输出一个图形&#xff0c;然后Very Beautiful。11 打印字母C 11 用*号输出字母C的图案。 讲道理这绝对不该是个新人能整出来的活儿&#xff0c…