300 model never mentions processes explicitly. The other parameters are |
300 model never mentions processes explicitly. The other parameters are |
301 provided as arguments by the caller; the @{term path} one is common |
301 provided as arguments by the caller; the @{term path} one is common |
302 to all kinds of system-calls. |
302 to all kinds of system-calls. |
303 *} |
303 *} |
304 |
304 |
305 primrec |
305 primrec uid_of :: "operation \<Rightarrow> uid" |
306 uid_of :: "operation \<Rightarrow> uid" |
|
307 where |
306 where |
308 "uid_of (Read uid text path) = uid" |
307 "uid_of (Read uid text path) = uid" |
309 | "uid_of (Write uid text path) = uid" |
308 | "uid_of (Write uid text path) = uid" |
310 | "uid_of (Chmod uid perms path) = uid" |
309 | "uid_of (Chmod uid perms path) = uid" |
311 | "uid_of (Creat uid perms path) = uid" |
310 | "uid_of (Creat uid perms path) = uid" |
312 | "uid_of (Unlink uid path) = uid" |
311 | "uid_of (Unlink uid path) = uid" |
313 | "uid_of (Mkdir uid path perms) = uid" |
312 | "uid_of (Mkdir uid path perms) = uid" |
314 | "uid_of (Rmdir uid path) = uid" |
313 | "uid_of (Rmdir uid path) = uid" |
315 | "uid_of (Readdir uid names path) = uid" |
314 | "uid_of (Readdir uid names path) = uid" |
316 |
315 |
317 primrec |
316 primrec path_of :: "operation \<Rightarrow> path" |
318 path_of :: "operation \<Rightarrow> path" |
|
319 where |
317 where |
320 "path_of (Read uid text path) = path" |
318 "path_of (Read uid text path) = path" |
321 | "path_of (Write uid text path) = path" |
319 | "path_of (Write uid text path) = path" |
322 | "path_of (Chmod uid perms path) = path" |
320 | "path_of (Chmod uid perms path) = path" |
323 | "path_of (Creat uid perms path) = path" |
321 | "path_of (Creat uid perms path) = path" |
347 via transitions of the file-system configuration. This is expressed |
345 via transitions of the file-system configuration. This is expressed |
348 as an inductive relation (although there is no actual recursion |
346 as an inductive relation (although there is no actual recursion |
349 involved here). |
347 involved here). |
350 *} |
348 *} |
351 |
349 |
352 inductive |
350 inductive transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" |
353 transition :: "file \<Rightarrow> operation \<Rightarrow> file \<Rightarrow> bool" |
351 ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) |
354 ("_ \<midarrow>_\<rightarrow> _" [90, 1000, 90] 100) |
|
355 where |
352 where |
356 |
|
357 read: |
353 read: |
358 "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow> |
354 "access root path uid {Readable} = Some (Val (att, text)) \<Longrightarrow> |
359 root \<midarrow>(Read uid text path)\<rightarrow> root" | |
355 root \<midarrow>(Read uid text path)\<rightarrow> root" | |
360 "write": |
356 "write": |
361 "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow> |
357 "access root path uid {Writable} = Some (Val (att, text')) \<Longrightarrow> |
498 relation describes the cumulative effect of the sequence of |
494 relation describes the cumulative effect of the sequence of |
499 system-calls issued by a number of running processes over a finite |
495 system-calls issued by a number of running processes over a finite |
500 amount of time. |
496 amount of time. |
501 *} |
497 *} |
502 |
498 |
503 inductive |
499 inductive transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" |
504 transitions :: "file \<Rightarrow> operation list \<Rightarrow> file \<Rightarrow> bool" |
500 ("_ =_\<Rightarrow> _" [90, 1000, 90] 100) |
505 ("_ =_\<Rightarrow> _" [90, 1000, 90] 100) |
|
506 where |
501 where |
507 nil: "root =[]\<Rightarrow> root" |
502 nil: "root =[]\<Rightarrow> root" |
508 | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" |
503 | cons: "root \<midarrow>x\<rightarrow> root' \<Longrightarrow> root' =xs\<Rightarrow> root'' \<Longrightarrow> root =(x # xs)\<Rightarrow> root''" |
509 |
504 |
510 text {* |
505 text {* |
628 Rather obviously, a list of system operations can be executed within |
623 Rather obviously, a list of system operations can be executed within |
629 a certain state if there is a result state reached by an iterated |
624 a certain state if there is a result state reached by an iterated |
630 transition. |
625 transition. |
631 *} |
626 *} |
632 |
627 |
633 definition |
628 definition "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
634 "can_exec root xs = (\<exists>root'. root =xs\<Rightarrow> root')" |
|
635 |
629 |
636 lemma can_exec_nil: "can_exec root []" |
630 lemma can_exec_nil: "can_exec root []" |
637 unfolding can_exec_def by (blast intro: transitions.intros) |
631 unfolding can_exec_def by (blast intro: transitions.intros) |
638 |
632 |
639 lemma can_exec_cons: |
633 lemma can_exec_cons: |