2023年11月25日

编程代写｜CSC8204: Coursework (SPARK Ada)

这是一篇关于为了提高对常见编程错误的理解和解决率，实践火花分析和证明工具，获得编写信息流和证明方面的经验，并计算最弱的先决条件，以获得简单代码示例的验证条件的编程代写

 

Submission details:

Submit your solution to Ness by the deadline (Thu Dec 15, 15:30). Your solution should consist of a zip file containing:

  • A document (word, text or pdf) with your answers to the questions below
  • Updated stack.ads, stack.adb and test_stack.adb files.

This exercise is marked out of 50, and contributes 100% of the assessment for this module. It consists of 4 tasks.

The coursework uses the Stack project which was used in the tutorial. You should begin with a fresh copy of the tutorial, downloaded from canvas.

Task 1: Correcting the test code [5 marks]

This task involves checking and fixing the Ada code in the test_stack file.

When you compiled and ran the test_stack program in the tutorial, you may have noticed it has a subtle bug. The first loop in the code takes keyboard input and adds integers to the stack, until a 0 is entered. This causes the loop to terminate, but the 0 is also added to the content of the stack (as can be seen in the second loop, which prints out the stack contents).

Modify the code so that the 0 is not added to the stack. In other words, for input:

The stack content output should be: Stack contents: 9 12 8 10

In your document, provide a copy of the new version of the test_stack procedure. [5 marks]

Task 2: Adding specification contracts [15 marks]

The stack.ads file has Global and Depends aspects for all the functions and procedures. Your task is to add proof aspects to the specification so that each function and procedure has a Post  aspect and, if necessary, a Pre aspect, which specifies the correct behaviour of the code. Run the SPARK examiner and prover to help you check your postconditions.

In your document, provide a copy of the updated stack.ads file. [15 marks]

Task 3: The Swap Procedure [20 marks]

We can now extend the Stack package to add another procedure, Swap. This will take two integer parameters, I and J, as indexes of the stack, and exchange the values in the stack at these index points. You are given the executable code, your task is to add the specification of the procedure:

a) Add the following code to the body, adb: 

procedure Swap(I, J: in Pointer_Range) is

Temp: Integer;

begin

if(I <= Pointer) and (J <= Pointer) then

Temp := S(I);

S(I) := S(J);

S(J) := Temp;

end if;

end Swap;

The procedure will only swap over the values if I and J are within the current size of the stack; otherwise, the stack is unchanged.

b) In the specification ads, add the specification for the procedure:

procedure Swap(I, J: in Pointer_Range) with Complete the specification by adding Global, Depends, Pre, Post or Contract_Cases aspects to specify the expected behaviour of the procedure.

In your document, provide a copy of the specification of the Swap procedure. [15 marks]

c) Now consider the following alternative implementation of the Swap procedure:

procedure Swap(I,J: in Pointer_Range) is

Temp1: Integer;

Temp2: Integer;

begin

if(I <= Pointer) and (J <= Pointer) then

Temp1 := S(I);

Temp2 := S(J);

S := Vector'(Index_Range => 0); — set all contents of S to 0

S(J) := Temp1;

S(I) := Temp2;

end if;

end Swap;

This implementation differs from the original one, as it destroys the contents of the stack except for the values at the index points I and J, which are preserved and swapped. This is not what we would expect a Swap procedure to do – but is your specification satisfied by this implementation? In other words, does your specification describe correct behaviour and rule out incorrect behaviour?

In your document, answer the following question:

Does your specification rule out the above “wrong” implementation? If you believe it does, explain why. If you believe does not, explain what you need to change in the specification to rule out this implementation.  [5 marks]

Task 4: Weakest preconditions [10 marks]

Use the process of postcondition hoisting and proof rules for sequence and assignment to derive the weakest preconditions and the verification conditions for the following specification statements. Be sure to show each step in the derivation process.

{ true }

M := X;

N := Y;

A := 2 * M + N;

N := N – 1;

M := A

{ M > N}

[10 marks]

Provide the answer to this question in your document.

Make sure you include your answers to all tasks in the word, text or pdf document you submit – and include the final versions of the specification and body files in your submission.