whispertzx

我们研一的九月   研究生的第一个月很快就过去了，我和她研一的九月也过去了～～～

汇报内容1、汇报formal method书第二章：（1）首先引入GC的概念，然后使用BNF范数进行定义，通过第一章对于PG的基本介绍，扩充PG的基本操作，引入GC至PC中，并定义edges函数，然后结构和第一章一致，引入GC的概念。 （2）什么是语义：语言所表达的含义，也就是这句话（这条语句）所表达的意思。 （3）什么是语法：语言的结构规则，也就是怎么样写一段是对的。 （4）什么是语法糖：糖不改变其所在位置的语法结构下实现了运行时等价，作用简写不限于此。 （5）什么是指称语义：把程序的意义映射到某种数学结构，这种结构能清晰地表达程序对环境的作用和环境的变化。 （6）什么是操作语义：把程序运行看作了执行一系列改变环境的操作，用一组描述环境变化的规则定义程序中各种结构的意义。 2、汇报社会保障、切尔诺夫不等式： 智利国家的社会保障制度的特点，切尔诺夫不等式的一个逼近。 导师反馈内容1、如何进行学习：找一堆文章—->按照文章下面推荐的进行找—->进行筛选—->对文章进行打标签 2、refinement：精化。粗粒度—->细粒度？？？ 上界：所有条件均符合；下界：所有 ...

汇报内容1、汇报formal method书第一章：（1）第一章PG（程序图）用来定义程序和系统的控制结构，类似于有向图。定义了Q点集、ACT行为、E边集。然后引入了有限自动机的概念，将PG与有限自动机对应起来，将自动机转移状态对应PG的边。但是与程序流程图有一定差异。（2）接着引入语义S[[.]]，使用S将ACT行为明确，也就是拿上一步各个数据，通过ACT行为后修改对应变量数据后内存各个数据的状况。举例如何使用PG来表示，非确定系统和没有成功终止的系统，接着引入sita符号表示程序过程的内存状态。接着就是DS和ES（确定系统和演化系统）概念，定义语义和语言就能形成一种语言。 导师反馈内容1、程序图静态、语义模型动态（解决是否等价、执行过程是否一致）2、{指称语义（将其转化为数学对象，例如CSP的traces）、操作语义（状态迁移系统、可达性）、代数语义}。=>语义模型。其中对指称语义和操作语义的主要形式和优点进行总结，分析经典模型等的概念和优点。3、如何学习，了解物理上的场景（如何运作），对论文中、现实中的关注的核心问题进行建模->抽离简易问题，提炼核心问题->学完 ...

汇报内容1、提问形式化验证的方向：（1）定理证明器：将主流算法等用形式化语言编写，并加以证明。（2）模型检测：将主流系统或算法进行建模，使用建模工具进行验证，可判定问题、完备性。2、目标和方向3、如何寻找形式化方向的论文，书本看的选择4、本周主要是学习课程，在进程代数和系统分析与验证中，对KS建模，一阶谓词逻辑等进行学习 导师反馈内容1、软件工程的需求，形式化验证是实现需求，用数学语言定义需求等。在形式化中，越来越多的工业软件在使用，除了航空航天，还有自动驾驶、轨道交通等。2、可信方面上数学主要是以统计和优化为主。3、人工智能的可解释性可以从：X-AI（explain AI）4、形式化验证文章：CAV/TACAS/FSE ｜ICSE/ICFEM｜FAC/理论计算机科学5、计算机逻辑基础的某一章讲述的CTL是Model Checking；Model Checking书较为简单；principle of Model Checking理论、数学较强，较难理解。6、Formal method和程序理论配合着看。7、对于书进行解释，需要用自己的语言进行组织来阐述。

汇报内容上周对论文《An Efficient Coq Tactic for Deciding Kleene Algebras》进行解读，首先将Kleene Algebras使用符号进行解释，其次对Kleene Algebras的符号表示使用有限自动机理论进行解释，其中自动机理论转化为正则表达式进行解释。1、决定Kleene Algebras中的等式有限自动机理论：正则语言相等条件，当且仅当相应的最小自动机是同构的。表达式a,b表示相同的正则语言，那么在任意Kleene Algebras中都能证明a=b。Kleene Algebras中的A元素可以有三个矩阵表示<u,m,v>，其中u,v是0-1向量，M表示转化矩阵，u为初始态，v为接受态，Kleene Algebras上的方阵形成Kleene Algebras。 2、潜在的设计选择定义代数层级、矩阵表示、异构结构处理、物化机制、数字表示。代数层级Kleene Algebras{单类：monoid，半格：semi-lattice}。矩阵：整数对->type X的部分映射。类型化代数、类型具体化（类型具体化coq不处理类型结 ...

长沙行  大四狗终于毕业了，去长沙吃喝玩乐去了。因为不知道写啥，只好用图片展示啦~~

关于我的本科毕业设计  前几天本科毕业答辩终于结束了，这篇文章就讲一下我的本科毕业设计情况。  我们学校大约在一月初的时候开始选题，我做的是自己的指导老师给的题目(自己一开始不知道该怎么选题，看看还是直接做指导老师给的)，主要是关于图像修复方面的，我一开始心想，woc这个我怎么可能会做，怕不是老师搞我吧，后来导师给我找了一个博士生，让我不懂的可以问他(学长人真的nice，我感觉要是我学长的话，我就会觉得这个师弟怎么这么菜，啥都不知道，事情还贼多，周末还找我，这不是影响我打游戏嘛！！！)。就这样，我开始了我的毕业设计之旅。  一开始觉得时间还很长，毕竟六月份才答辩，还有半年，开题报告也是三月份才检查，一月份我炒鸡认真，我心想，我赶紧把开题啊文献综述啊什么的写好，然后再花一个月写毕业设计代码，还剩四个月，那不是开开兴兴玩玩玩？？？然后一鼓作气，再而衰，三而竭，我就坚持了三天(哦不，这能叫坚持嘛？)，放弃了。图像修复远远没有那么容易理解，大概水了一个多月的时间，到了不得不写的时候，终于开始奋斗了，什么图像修复、去噪、数据、MATLA ...

java支持的数据类型有哪些？什么是自动拆箱和装箱 java支持基本数据类型和引用数据类型。基本数据类型有八种，分别为 int char double float boolean short long byte。除了基本数据类型都是引用数据类型比如 string。 自动拆箱就是把包装类型的数据转化成基本数据类型，自动装箱就是把基本数据类型转化为包装数据类型。比如：int -> Integer基本数据类型比如int默认值是0，而Integer默认值是null，Integer必须实例化之后才能使用，并且存储的是指向该对象的引用。在比较中，new Integer之间的比较是false；对于非new Integer和new的进行对比，由于非new的指向的常量池中的，new的是指向新建的堆中的，所以地址不一样，是false； 对于两个非new生成的Integer对象，进行比较时，如果两个变量的值在区间-128到127之间，则比较结果为true，如果两个变量的值不在此区间，则比较结果为false。 什么是值传递，什么是引用传递 值传递是对于基本型变量而 ...

软硬件配置Mac电脑版本：macOS Catalina 10.15.07TensorFlow版本：1.9.0python：3.6.5 python环境搭建下载python3.6.5并安装，安装完毕后修改bash.profile文件将python3.6.5版本设置为使用的python路径。使用open .bash_profile打开配置文件，如果没有请创建 1open .bash_profile 并在末尾添加以下代码： 1alias python="/Library/Frameworks/Python.framework/Versions/3.6/bin/python3.6" 成功后使用python –version查看版本是否正确。 1python --version TensorFlow创建虚拟环境本文使用的是虚拟环境virtualenv，首先创建虚拟环境 12sudo pip install virtualenv或者是sudo pip3 install virtualenv 其次创建 ...