CTEC5721/ 2  Software  Evolution

 

Coursework  Resit 3

 

There are three parts. Please complete all three parts. Every student needs to undertake  these  parts individually.

 

Part  A: 20 Marks (Due date:  5:00pm  Friday 2nd  September  2016)

Part Al

Program  P1 is:

do if  n     0 then  exit   fi;

if  even (n) then  n := n – 2 else n := n + 1 fi od

Program  P2 is:

do if  n     0 then  exit fi;

n := n – 1od

Let n0 be the initial value of n. Prove, by induction on n0 that the two programs are equivalent  for all non-negative  integer values of no.  (5  marks).

The bodies of these two loops are combined to form program P3 which is: do if n        0 then  exit  fi;

if  even (n)  then  n := n – 2 else n := n + 1 fi;

if n     0 then  exit  fi;

n := n – 1 od

Is P3 equivalent to P1 and P2? Either prove  that  they  are equivalent,  or  find an initial  state for which  P3 gives  a different  result  to P1.  (5  marks).

 

Part A2

Program  P4  is:

do if ,B then  exit(l)  fi;

do if B  I  B1 then  S1 else exit(l) fi od;

do if B I      B1 then  S2  else exit(l) fi od od

Program  P5 is:

do if ,B then  exit(l)  fi;

if B1 then S1 else S2  fi od

where statements S1 and S2 are proper sequences: i.e. they do not contain any exits which could terminate any enclosing  loops.

Convert P4 and P5 to regular action  systems,  removing  the loops and  taking  all code out of the bodies of if statements, so that the body of each if statement contains only action calls. Transform the action systems to prove that the two programs  are  equivalent.   (10 marks).

 

 

 

Part  B: 30 Marks  ( Due  date:  5:00pm  Friday 2nd  September   2016)

This part of the coursework is to ask you to experiment with program trans­ formation techniques on the FermaT tool. The aim is to restructure a program and improve the quality  of the program  by  applying  transformations.

The program you will be working on is f mt008a .wsl which is on the Blackboard system:

var (Flagl := 0, Flag2 := 0, last := “”, record := “”, cha nged := 0) : last := na me[i];

i := (i + 1);

while na me[i] i- “” do

if Flag2 = 0  V  last i-  na me[i]

then if Flagl = 1

then  if tota I   i- 0

then  !P write(last, tota l   var sys);

cha nged := (cha nged + 1) fi fi;

Flagl := 1; tota l  := O;

tota l  := (tota l  + n u m ber[i]);

Flag2 := 1

else tota l := (tota l + n u m ber[i]); Flag2  := 1 fi;

last := na me[i]; i := (i + 1) od;

if Flag2 = 1

then  if tota I   i- 0

then !P write(last, tota l  var sys); cha nged := (cha nged + 1) fi fi;

!P write( “Changed :”, cha nged var sys)

end

Try to aim for a result that looks like f mt008b .wsl (which is also on the Black­ board system):

var (cha nged := 0) : i := (i + 1);

while na me[i] i- “” do

tota l := n u m ber[i]; i  :=  (i + l);

while na me[(i – 1)] = na me[i] I na me[i] i- “” do

tota l := ( n u m ber[i] + tota l ); i := (i + 1)   od;

if tota l  i- 0

then !P write( na me[(i – 1)], tota l var sys); cha nged  := (cha nged + 1)  fi od;

!P write( “Changed :”, cha nged var sys)

end

Your  report  on the transformation  process  should  list  all the steps taken   and

 

 

 

briefly justify each step. You are expected to know why a particular transfor­ mation improves or simplifies the program. You may include a few intermediate versions of the program for illustration: it is not necessary to include a copy of the program after every transformation, you need to decide which intermediate versions  illustrate  the most  important  steps in the process.

Note: You must not use the Flag_Remova l transformation. Flags can be removed manually   using  other  transformations.

 

Part  C: 50  Marks  ( Due  date:  5:00pm  Friday  2nd  September 2016)

• Please write a research report of 5,000 to 6,000 words (excluding figures and references) on the topic of “Theory and Practice of Formal Methods Applied to Software Evolution”.

You should discuss a number of different formal methods, comparing and contrasting them with special reference to their application to software evolution. In particular, for each of the methods you describe, you should discuss: ( 1) Can programs developed using this formal method also be re-engineered using this method? and (2) Can  existing  programs,  which were not developed using any particular formal method, be re-engineered using  this  method?

References must be properly  supplied.

• An electronic copy of your report in the form of a CD needs to be handed in at the same time as the report, which will be checked by a plagiarism detection

 

Marking

1. Abstract, Introduction, Format and Language  {10 marks)
2. Relevance and Significance{lO marks)
3. Technical Quality {20 marks)
4. Critical thoughts, Summary and Conclusions {10 marks)