equal
deleted
inserted
replaced
841 bogus situation in an abstract manner: located at a certain @{term |
841 bogus situation in an abstract manner: located at a certain @{term |
842 path} within the file-system is a non-empty directory that is |
842 path} within the file-system is a non-empty directory that is |
843 neither owned nor writable by @{term user\<^isub>1}. |
843 neither owned nor writable by @{term user\<^isub>1}. |
844 *} |
844 *} |
845 |
845 |
846 definition |
846 |
|
847 |
|
848 definition invariant where |
847 "invariant root path = |
849 "invariant root path = |
848 (\<exists>att dir. |
850 (\<exists>att dir. |
849 access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
851 access root path user\<^isub>1 {} = Some (Env att dir) \<and> dir \<noteq> empty \<and> |
850 user\<^isub>1 \<noteq> owner att \<and> |
852 user\<^isub>1 \<noteq> owner att \<and> |
851 access root path user\<^isub>1 {Writable} = None)" |
853 access root path user\<^isub>1 {Writable} = None)" |