Back - Formal Specification | Previous - Academic Administrator | Next - Weather Map

Tutorial Solutions - Filing Subsystem

 

Asked to identify and correct the flaw in each line.

Corrections are as below.

Note - there is no correction needed in line 3 of the predicate.

ÚÄFileSystemÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
owns : users FileNames
occupies : FileNames BlockNos
SystemUsers : users
FreeBlocks : BlockNos
NoUsers :
ÃÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄ
# SystemUsers ó NoUsers
" file : dom occupies $ us : dom owns file î owns us
" file : dom occupies; block : BlockNos block î occupies file Î block ç FreeBlocks
dom owns = SystemUsers
" fs1,fs2 : ran owns fs1 fs2 Î fs1 fs2 = í
ÀÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÄÙ