Master d’informatique 2006 2007 de l’université Paris VI
cps
ADT pour les Cuves

Cuve bornée : approche défensive

Service : BoundedBucket

Types : boolean, double

Constructors :

init: double -> [BoundedBucket]
   precondition: init(l) require l>0

Observators :

 getBound: [BoundedBucket] -> double
 getQuantity: [BoundedBucket] -> double
 isEmpty: [BoundedBucket] -> boolean
 isFull: [BoundedBucket] -> boolean

Operations :

 fill: [BoundedBucket] * double -> [BoundedBucket]
   precondition: fill(B,l) require l>=0 /\ getQuantity(B)+l <= getBound(B)

 pump:  [BoundedBucket] * double -> [BoundedBucket]
   precondition: pump(B,l) require l>=0 /\ getQuantity(B)-l >= 0

Axioms :

Global
- getBound(B)>0
- getQuantity(B)>=0  /\  getQuantity(B)<=getBound(B)
- isEmpty(B) = [ getQuantity(B) = 0 ]
- isFull(B) = [ getQuantity(B) = getBound(B) ]

init
- getBound(init(l)) = l
- getQuantity(init(l)) = 0

fill
- getBound(fill(B,l)) = getBound(B)
- getQuantity(fill(B,l)) = getQuantity(B)+l

pump
- getBound(pump(B,l)) = getBound(B)
- getQuantity(pump(B,l)) = getQuantity(B)-l

Cuve bornée : approche permissive

Service : BoundedBucket

Types : boolean, double

Constructors :

init: double -> [BoundedBucket]
   precondition: init(l) require l>0

Observators :

 getBound: [BoundedBucket] -> double
 getQuantity: [BoundedBucket] -> double
 isEmpty: [BoundedBucket] -> boolean
 isFull: [BoundedBucket] -> boolean

Operations :

 fill: [BoundedBucket] * double -> [BoundedBucket]
   precondition: fill(B,l) require l>=0

 pump:  [BoundedBucket] * double -> [BoundedBucket]
   precondition: pump(B,l) require l>=0

Axioms :

Global
- getBound(B)>0
- getQuantity(B)>=0  /\  getQuantity(B)<=getBound(B)
- isEmpty(B) = [ getQuantity(B) = 0 ]
- isFull(B) = [ getQuantity(B) = getBound(B) ]

init
- getBound(init(l)) = l
- getQuantity(init(l)) = 0

fill
- getBound(fill(B,l)) = getBound(B)
- getQuantity(fill(B,l)) = min(getBound(B),getQuantity(B)+l)

pump
- getBound(pump(B,l)) = getBound(B)
- getQuantity(pump(B,l)) = max(0,getQuantity(B)-l)

Tuyau

Service : Pipe

Types : boolean, int, double

Require : BoundedBucket (connector)

Constructors :

init : double  -> [Pipe]
        precondition : init(r) require r > 0

Observators :

 getRate : [Pipe] -> double

 getClock : [Pipe] -> int

 isBoundIn : [Pipe] -> boolean  (connector)

 isBoundOut : [Pipe] -> boolean  (connector)

 isBound : [Pipe] -> boolean  (connector)

 getIn : [Pipe] -> BoundedBucket   (connector)

 getOut : [Pipe] -> BoundedBucket (connector)

Operations :

 bindIn : [Pipe] * BoundedBucket -> [Pipe]  (connector)
   precondition : bindIn(P,B) require not isBoundIn(P) /\ B<>null

 unbindIn : [Pipe] -> [Pipe]   (connector)
   precondition : unbindIn(P) require isBoundIn(P)

 bindOut : [Pipe] * BoundedBucket -> [Pipe]   (connector)
   precondition : bindOut(P,B) require not isBoundOut(P) /\ B<>null

 unbindOut : [Pipe] -> [Pipe]    (connector)
   precondition : unbindOut(P) require isBoundOut(P)

 step : [Pipe] -> [Pipe]
   precondition : step(P) require isBound(P)
 
 step : [Pipe] * int -> [Pipe]
   precondition : step(P,n) require isBound(P) /\ n>0

Axioms :

Global
- getRate(P) > 0
- getClock(P) >= 0
- isBound(P) = (isBoundIn(P) /\ isBoundOut(P))
- isBoundIn(P) =  (getIn(P)<>null)
- isBoundOut(P) = (getOut(P)<>null)

init
- getRate(init(r)) = r
- getClock(init(r)) = 0
- getIn(init(r)) = null (connector)
- getOut(init(r)) = null (connector)

bindIn
- getRate(bindIn(P,B)) = getRate(P)
- getClock(bindIn(P,B)) = getClock(P)
- getIn(bindIn(P,B)) = B (connector)
- getOut(bindIn(P,B)) = getOut(P) (connector)

unbindIn
- getRate(unbindIn(P)) = getRate(P)
- getClock(unbindIn(P)) = getClock(P)
- getIn(unbindIn(P)) = null (connector)
- getOut(unbindIn(P)) = getOut(P) (connector)

bindOut
- getRate(bindOut(P,B)) = getRate(P)
- getClock(bindOut(P,B)) = getClock(P)
- getIn(bindOut(P,B)) = getOut(P) (connector)
- getOut(bindOut(P,B)) = B (connector)

unbindOut
- getRate(unbindOut(P)) = getRate(P)
- getClock(unbindOut(P)) = getClock(P)
- getIn(unbindOut(P)) = getIn(P) (connector)
- getOut(unbindOut(P)) = null (connector)

step/1
- getRate(step(P)) = getRate(P)
- getClock(step(P)) = getClock(P)+1
- getIn(step(P)).getQuantity() = getIn(P).getQuantity()-getRate(P) (connector)
- getOut(step(P)).getQuantity() = getOut(P).getQuantity()+getRate(P) (connector)

step/2
- getRate(step(P,n)) = getRate(P)
- getClock(step(P,n)) = getClock(P)+n
- getIn(step(P,n)).getQuantity() = getIn(P).getQuantity()-(getRate(P)*n) (connector)
- getOut(step(P,n)).getQuantity() = getOut(P).getQuantity()+(getRate(P)*n) (connector)