COMP 317: Semantics of Programming Languages

1. Specify, implement, and prove the correctness of a program that swaps the array values a['x] and a['y].
   In the precondition, you can either specify the initial values of a['x] and a['y]:

     var S : Store .
     vars X Y : Int .
     eq  pre(S,X,Y)  =  (S[[ a['x] ]]) is X and (S[[ a['y] ]]) is Y .
   

   or you can specify the inital value of the array variable a:

     var S : Store .
     var A : Array .
     eq  pre(S,A,X,Y)  =  (S[[ a ]]) == A  and  (S[['x]]) is X  and ...
   

   (in which case, the postcondition should state that, in the store S that results from running the program, S[[ a['x] ]] is A[Y], etc.).
    
2. Specify, implement, and prove the correctness of a program that for all i (with 0 <= i < 99) sets a[i] to i.
    
3. Define a Maude operation arraySum that takes an Array and an Int and returns an Int such that for all arrays A and Ints L

       arraySum(A,L)  =  A[0] + A[1] + ... + A[L - 1] .
   

   Use this to specify a program that sets 's to the sum of the values a[0] + a[1] + ... + a[99]. Implement and prove the correctness of your program.