Transcript Introduction to Event

CSC 4504 : Langages formels et applications
(La méthode Event-B)
J Paul Gibson, A207
[email protected]
http://www-public.it-sudparis.eu/~gibson/Teaching/Event-B/
PurseCode
http://www-public.it-sudparis.eu/~gibson/Teaching/Event-B/PurseCode.pdf
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.1
Java implementation of Purse requirements
public class Purse {
int numberCoinTypes;
int [] CoinTypes;
int [] Coins;
….
}
Why do we say that the Java code is less formal than the Event-B
model?
Do you think the code is correct?
2009: J Paul Gibson
(Available on web – Purse.java)
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.2
Java implementation of Purse requirements
Purse (int nct, int largest, int maxnumber){
System.out.print("Constructing Random Purse with "+nct+" coin types, largest possible coin
value "+largest);
System.out.println(", and \n(initially) no more than "+maxnumber+ " coins of same type in
the purse" );
numberCoinTypes = nct;
CoinTypes = new int [nct];
Coins = new int [nct];
for (int i=0; i<numberCoinTypes; i++) Coins[i] =(int) (Math.random()*maxnumber+1);
for (int i=0; i<numberCoinTypes; i++) {
int temp = 0;
do {
temp = (int) (Math.random()*largest+1);
} while ((isCoin(temp)));
CoinTypes [i] = temp;
}
} //Purse constructor
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.3
Java implementation of Purse requirements
public int howManyCoins(int c){
for (int i=0; i<numberCoinTypes; i++)
if (c == CoinTypes [i]) return Coins[i];
return 0;
}
public void addCoin (int c){
for (int i=0; i<numberCoinTypes; i++)
if (CoinTypes[i] == c) Coins[i]++;
}
public void removeCoin (int c){
for (int i=0; i<numberCoinTypes; i++)
if (CoinTypes[i] == c && Coins[i]>0) Coins[i]--;
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.4
Java implementation of Purse requirements
// add a random coin
public void addCoin (){
Coins[ (int) (Math.random()* numberCoinTypes)]++;
}
// randomly remove a coin
public void removeCoin (){
if (total()==0) return;
int temp = (int) (Math.random()* numberCoinTypes);
if (Coins[temp] >0) Coins[temp]--;
else removeCoin();
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.5
Java implementation of Purse requirements
// add a random coin
public void addCoin (){
Coins[ (int) (Math.random()* numberCoinTypes)]++;
}
// randomly remove a coin
public void removeCoin (){
if (total()==0) return;
int temp = (int) (Math.random()* numberCoinTypes);
if (Coins[temp] >0) Coins[temp]--;
else removeCoin();
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.6
Java implementation of Purse requirements
// NOT USED IN PORGRAM BUT TIES INTO SPECIFICATION
public boolean hasSubPurse(Purse p2){
for (int i=0; i<numberCoinTypes; i++){
if (Coins[i]< p2.howManyCoins(Coins[i]) )
return false;
}
return true;
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.7
Java implementation of Purse requirements
public boolean paySum(int sum, Purse p){
if (sum>total())
return false;
if (isCoin(sum) && howManyCoins(sum) >0 ){
p.removeCoin(sum);
System.out.print(" "+ sum );
return true;}
else {
for (int i = 0; i<numberCoinTypes; i++){
if (howManyCoins(CoinTypes[i]) >0){
p.removeCoin(CoinTypes[i]);
if ( sum-CoinTypes[i]>0 && p.paySum(sum-CoinTypes[i], p)){
System.out.print(" "+ CoinTypes[i]);
return true;}
else p.addCoin(CoinTypes[i]);
}
}
return false;
}
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.8
Java implementation of Purse requirements
public int total(){
int t =0;
for (int i=0; i<numberCoinTypes; i++)
t = t+ CoinTypes[i]* Coins[i];
return t;
}
public boolean isCoin(int c){
for (int i=0; i<numberCoinTypes; i++)
if (CoinTypes[i] == c) return true;
return false;
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.9
Java implementation of Purse requirements
public String toString (){
String result ="";
for (int i=0; i<numberCoinTypes; i++)
result = result + CoinTypes[i]+"->"+ Coins[i]+ " ";
result =result+":: Total = "+ total();
return result;
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.10
Java implementation of Purse requirements
public static void main(String[] args) {
System.out.println("Test Purse Class");
Purse p = new Purse (4, 20, 3);
System.out.println(p);
int s = (int) (Math.random()*50)+1;
System.out.println("\nTrying to pay "+ s);
if (p.paySum(s, p)) System.out.println("\nPaid sum required\n");
else
System.out.println("\nCan't pay sum required\n");
System.out.println(p);
}
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.11
Java implementation of Purse requirements
Execution 1:
Test Purse Class
Constructing Random Purse with 4 coin types,
largest possible coin value 20, and
(initially) no more than 3 coins of same type
in the purse
20->1 7->3 8->2 9->2 :: Total = 75
Trying to pay 4
Can't pay sum required
20->1 7->3 8->2 9->2 :: Total = 75
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.12
Java implementation of Purse requirements
Execution 2:
Test Purse Class
Constructing Random Purse with 4 coin types,
largest possible coin value 20, and
(initially) no more than 3 coins of same type
in the purse
18->1 15->3 6->2 13->2 :: Total = 101
Trying to pay 50
13 13 6 18
Paid sum required
18->0 15->3 6->1 13->0 :: Total = 51
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.13
Java implementation of Purse requirements
Execution 3:
Test Purse Class
Constructing Random Purse with 4 coin types,
largest possible coin value 20, and
(initially) no more than 3 coins of same type
in the purse
19->1 5->3 18->2 11->3 :: Total = 103
Trying to pay 10
5 5
Paid sum required
19->1 5->1 18->2 11->3 :: Total = 93
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.14
How easy is it to verify the Java Code?
Question: does Java code help you better understand the
requirements?
Question: can it help you to write the requirements in Event-B?
Challenge: try to hide a bug in code (in a 2nd version). Also make
changes to code (in a 3rd version) that dont add a bug. Ask a
colleague to say which version is bugged. HINT: To make it harde
make sure that both new versions pass my simple test code.
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.15
Purse specification in Event-B
Purse_ctx0 : all proof obligations discharged
TO DO: Add theorems to validate add and remove functions
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.16
Purse specification in Event-B
Purse_ctx1 : not all proof obligations discharged
TO DO: Try to prove the unproved theorems (2,3 and 4)
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.17
Purse specification in Event-B
Purse_mch0 : all proof obligations discharged
TO DO: Think about how one could specify the pay_sum
event by stating what is required rather than how to do it
2009: J Paul Gibson
T&MSP-CSC 4504 : Langages formels et applications
Event-B/PurseCode.18