formal method lecture 7 文件系统

紫色的是变量的定义

红色的判断这些变量的判断

有两种方法能够做schema的操作

inclusion

有很多新的变量

说白了就是把两个schema拼在一起

这样也有很多的新的预测的点

我们能判断，这两组

有更强的判断的能力

这一个小符号

告诉其他的东西不变

这个原来的值是要改变的

唯一变化的地方

我们这个系统需要有很多的操作

要让老师能够知道你想表达啥

我们看看文件系统怎么做

看看我们怎么做一些操作

文件被用户拥有

每一个文件有一个文件地址

user的数量是有上界的

我们最简单的操作就是这个操作的type是啥

就跟找类一样

找一个set来装这些东西

我们后来回去看这些block都能干啥

先看看状态空间

那些block属于哪些地方？

哪些block是free的？

system_users是users的子集

owns是一个function能够mapping users 到files

occupies：是一个function能够把files做占据的blocks找到

frees_blocks是block的集合的子集

users的上界是自然数

————————

现在我们来看看的precaters怎么样

there is an upper bound to the number of users
#system_users<=no_users

files must be owned by someone

the blocks used to store files are not free for subsequent use

the blocks not used to store files are free

“#” 这个符号是说明了这个集合里面有多少个元素

dom的意思是domain

natural language的表达和不一定和predicate是一样的

考试的时候有很多的很多的解释的东西

说实话就是

这是一个能够加人的操作

说实话

总结

以上是生活随笔为你收集整理的formal method lecture 7 文件系统的全部内容，希望文章能够帮你解决所遇到的问题。

如果觉得生活随笔网站内容还不错，欢迎将生活随笔推荐给好友。