Dependent Information Flow Types

Examples from the paper (Conference Management System)

/***** Using GLOBAL Typedefs *******/

/** Ex 2.2  **/
typedef usr_type = { ref (Sigma[uid: int^BOT, name: int^U(uid), univ: int^U(uid), email: int^U(uid) ]^BOT)^BOT } ;;

typedef sub_type = { ref (Sigma[uid: int^BOT, sid: int^BOT, title: int^A(uid, sid), abst: int^A(uid, sid), paper: int^A(uid, sid) ]^BOT )^BOT  } ;;

typedef rev_type = { ref (Sigma[uid: int^BOT, sid: int^BOT, PC_only: int^PC(uid, sid), review: int^A(TOP, sid), grade: int^A(TOP, sid)]^BOT)^BOT };;

let Users = ref {}: usr_type ;;
let Submissions  = ref {}: sub_type ;;
let Reviews = ref {}: rev_type ;;
typedef ret_type = { Sigma[uid: int^BOT, sid: int^BOT, title: int^A(uida, sid), abst:int^A(uida, sid), 
						paper:int^A(uida, sid) ]^BOT } ;;

 let viewAuthorPapers = fun uida: int^BOT =>   		
	[ ret_type ]( foreach(x in !Submissions) with y = {}: ret_type do 
			    	let tuple = !x in
			    	  if(tuple.uid == uida) then tuple::y else y  ) ;;

 let n = 42 in (viewAuthorPapers(n)) ;;

/* Type: { Sigma[uid: int^BOT, sid: int^BOT, title: int^A(42, sid), abst: int^A(42, sid), paper: int^A(42, sid)]^BOT } */



/* Ex 2.3 */

typedef sub_elem = Sigma[uid: int^BOT, sid: int^BOT,  title: int^A(uid,sid), abst:int^A(uid,sid), paper:int^A(uid,sid) ]^BOT ;;


typedef sub = { sub_elem }  ;;

let viewAssignedPapers = fun uidr: int^BOT =>
	 	( foreach(x in !Reviews) with res_x = {}: sub do 
	   		let tuple_rev = !x 
	   		  in if(tuple_rev.uid == uidr ) then 
	   			   ( foreach(y in !Submissions) with res_y = {}: sub do 
					   let tuple_sub = !y
	   					in if(tuple_sub.sid == tuple_rev.sid) then tuple_sub::res_y else res_y )   
	   			 else res_x ) 
 
  ;;

 let r = first(viewAssignedPapers(42)) in r ;;
	  
/* Type: Sigma[uid: int^BOT, sid: int^BOT, title: int^A(uid, sid), abst: int^A(uid, sid), paper: int^A(uid, sid)]^BOT */
	  
	  
	  
	  
	  
/** Ex 2.4 **/


let t = first( 
    ( foreach(x in !Submissions) with y = {}: { int^A(42,70) } do 
	   let t_sub = !x in 
	     if(t_sub.uid == 42 and t_sub.sid == 70 ) then t_sub.title::y else y ))
         in foreach(x in !Submissions) with y = skip do  
		let t_sub = !x 
	    in if(t_sub.uid == 42 and t_sub.sid == 70) then 
	    	  let new_rec  = [uid: int^BOT = t_sub.uid, sid: int^BOT = t_sub.sid, 
	    		   			  title: int^A(uid, sid) = t, abst: int^A(uid, sid) = t_sub.abst, 
	    		   			  paper: int^A(uid, sid) = t_sub.paper ]
	    	  in x := new_rec ;;


/* Type: cmd^BOT */





/*** negative 2.4 ***/

 
 let t = first( ( foreach(x in !Submissions) with y = {}: { int^A(42,70) } do 
	   let t_sub = !x in 
	     if(t_sub.uid == 42 and t_sub.sid == 70 ) then t_sub.title::y else y) ) 
   in foreach(x in !Submissions) with y = skip do  
		let t_sub = !x 
	    in if(t_sub.uid == 32) then 
	    	  let new_rec  = [uid: int^BOT = t_sub.uid, sid: int^BOT = t_sub.sid, 
	    		   			  title: int^A(uid, sid) = t, abst: int^A(uid, sid) = t_sub.abst, 
	    		   			  paper: int^A(uid, sid) = t_sub.paper ]
	    	  in x := new_rec ;;


/* Wrong type: Expected declared type Sigma[uid: int^BOT, sid: int^BOT, title: int^A(uid, sid), abst: int^A(uid, sid), paper: int^A(uid, sid)]^BOT but found type Sigma[uid: int^BOT, sid: int^BOT, title: int^A(42, 70), abst: int^A(32, sid), paper: int^A(32, sid)]^BOT
 */




/** example between 2.4 and 2.5 from paper **/


typedef y_type =
   {Sigma[uid : int^BOT, sid : int^BOT, title: int^A(42,sid)]^BOT} in

 foreach (x in !Submissions) with y = {} : y_type do
   let t_sub = !x in
     if (t_sub.uid == 42) then
	[uid : int^BOT = t_sub.uid, sid : int^BOT = t_sub.sid,
	 title : int^A(42,sid) = t_sub.title] :: y
     else y
 ;;

/* Type: { Sigma[uid: int^BOT, sid: int^BOT, title: int^A(42, sid)]^BOT } */






/** Ex 2.5  **/

	   			 
   let comment = fun u: int^BOT, s: int^BOT, r: sub_elem =>
	   [ int^A(u,s) ] (if(r.uid == u and r.sid == s) then r.paper else 1) in   
    
    let addCommentSubmission = fun uid_r: int^BOT, sidr: int^BOT =>		
	 	( foreach(p in viewAssignedPapers(uid_r)) with dummy = skip do 
	   	    if(p.sid == sidr ) then 
	   		   ( foreach(y in !Reviews) with dummy2 = skip do 
				  let trev = !y in
	   				if(trev.sid == p.sid ) then 
	   				   ( let up_rec = [uid: int^BOT = trev.uid, 
	   								sid: int^BOT = trev.sid, 
									PC_only: int^PC(uid,sid) =  comment(p.uid, p.sid, p), 
	   								review: int^A(TOP, sid) = trev.review, 
	   								grade: int^A(TOP, sid) = trev.grade ] 
	   				   in y := up_rec ) ) )
    in addCommentSubmission;;
 
 
 /* Type: ( Pi(uid_r: int^BOT, sidr: int^BOT).(cmd^BOT) )^BOT */
 
 
 
 /***  negative 2.5 - without conditional in second foreach **/

	   			 
  let comment = fun u: int^BOT, s: int^BOT, r: sub_elem =>
	   [ int^A(u,s) ] (if(r.uid == u and r.sid == s) then r.paper else 1) in   
    
    let addCommentSubmission = fun uid_r: int^BOT, sidr: int^BOT =>		
	 	( foreach(p in viewAssignedPapers(uid_r)) with dummy = skip do 
	   	    if(p.sid == sidr ) then 
	   		   ( foreach(y in !Reviews) with dummy2 = skip do 
				  let trev = !y in
	   				   ( let up_rec = [uid: int^BOT = trev.uid, 
	   								sid: int^BOT = trev.sid, 
									PC_only: int^PC(uid,sid) =  comment(p.uid, p.sid, p), 
	   								review: int^A(TOP, sid) = trev.review, 
	   								grade: int^A(TOP, sid) = trev.grade ] 
	   				   in y := up_rec ) ) )
    in addCommentSubmission;;

/* Wrong type: Expected declared type Sigma[uid: int^BOT, sid: int^BOT, PC_only: int^PC(uid, sid), review: int^A(TOP, sid), grade: int^A(TOP, sid)]^BOT but found type Sigma[uid: int^BOT, sid: int^BOT, PC_only: int^A(TOP, sidr), review: int^A(TOP, sid), grade: int^A(TOP, sid)]^BOT
 */