紫色的是變量的定義

紅色的判斷這些變量的判斷

有兩種方法能夠做schema的操作

inclusion

有很多新的變量

說白了就是把兩個(gè)schema拼在一起

這樣也有很多的新的預(yù)測的點(diǎn)

我們能判斷，這兩組

有更強(qiáng)的判斷的能力

這一個(gè)小符號(hào)

告訴其他的東西不變

這個(gè)原來的值是要改變的

唯一變化的地方

我們這個(gè)系統(tǒng)需要有很多的操作

要讓老師能夠知道你想表達(dá)啥

我們看看文件系統(tǒng)怎么做

看看我們怎么做一些操作

文件被用戶擁有

每一個(gè)文件有一個(gè)文件地址

user的數(shù)量是有上界的

我們最簡單的操作就是這個(gè)操作的type是啥

就跟找類一樣

找一個(gè)set來裝這些東西

我們后來回去看這些block都能干啥

先看看狀態(tài)空間

那些block屬于哪些地方？

哪些block是free的？

system_users是users的子集

owns是一個(gè)function能夠mapping users 到files

occupies：是一個(gè)function能夠把files做占據(jù)的blocks找到

frees_blocks是block的集合的子集

users的上界是自然數(shù)

————————

現(xiàn)在我們來看看的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

“#” 這個(gè)符號(hào)是說明了這個(gè)集合里面有多少個(gè)元素

dom的意思是domain

natural language的表達(dá)和不一定和predicate是一樣的

考試的時(shí)候有很多的很多的解釋的東西

說實(shí)話就是

這是一個(gè)能夠加人的操作

說實(shí)話

總結(jié)

以上是生活随笔為你收集整理的formal method lecture 7 文件系统的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯(cuò)，歡迎將生活随笔推薦給好友。