Current section

Files

Jump to
pantagruel priv checkout.pant
Raw

priv/checkout.pant

module CHECKOUT.
user => User.
doc owner: User => Document.
" A specification for a small document management system.
check_out u:User, d:Document.
---
" A user may check out a document if they have permission to access it
" and it's not currently checked out.
(d.owner = nobody and (has_perm? u d)) -> d'.owner = u.
(d.owner != nobody or ~(has_perm? u d)) -> d'.owner = d.owner.
;
nobody :: User.
has_perm? u:User, d:Document :: Bool.