// コード2: ファイルアクセスプリミティブ
module FileIO
    // アクセスポリシーモジュールを読込
    open ACLs

    // canRead fがtrueと評価される（＝読み出し可能な）ファイル名fを引数に取り，string型の値（読み出した値）を返す関数readを定義
    assume val read : 
        f:filename{canRead f} -> string
    
    // canWrite fがtrueと評価される（＝書き込み可能な）ファイル名fとstring型の値（書き込む値）を引数に取り，unit型の値を返す関数writeを定義
    assume val write : 
        f:filename{canWrite f} -> string -> unit