Module Tycheck

module Tycheck: sig .. end

Type checking & conversion into command language

val args : (Arg.key * Arg.spec * Arg.doc) list

type state_predecessor = string * Exp.Id.t list * Assertions.cprop

type protocol_state = string * Exp.Id.t list * state_predecessor list * Exp.Id.t *
       Assertions.cprop

type protocol_item = {

	`protocol_name : string;`
	`protocol_states : protocol_state Misc.StringMap.t;`
	`protocol_successors : Misc.StringSet.t Misc.StringMap.t;`

}

type escrow_item = {

	`escrow_name : string;`
	`escrow_params : Exp.Id.t list;`
	`escrow_pre : Assertions.cprop;`
	`escrow_post : Assertions.cprop;`

}

val convert : Parsetree.p_item list ->
       (string list * Misc.StringSet.t * Exp.IdSet.t *
        (string, protocol_item) Hashtbl.t *
        (string, escrow_item) Hashtbl.t *
        (string, Commands.fun_info) Hashtbl.t *
        (Misc.component, Assertions.act list * Assertions.act list) Hashtbl.t *
        (Misc.component * Commands.res_init) list *
        (string * Commands.can_entailment) list)
       option

Returns (globals, protocols, fun_specifications, resources, res_initializers, fun_proofs)

Imprint | Data protection