For this assignment you will create a package named Buffers1.Homework1. This is a child package (named just Homework1) of the Buffers1 package. It must be defined in files named buffers1-homework1.ads and buffers1-homework1.adb. You do not need to modify in any way the original buffers1.ads and buffers1.adb files.
The code in a child package has direct visibility to the material in the parent package's specification. Specifically, the type definitions in the parent package are directly visible to the child. Ada developers can use child packages as a way of extending the functionality of a package. In the common case where a parent package is provided by a third party and cannot be edited, developers can effectively extend the parent package by definining suitable child packages.
Add the following declaration to the specification of Buffers1.Homework1:
procedure Immutable_Sort(Input : in Buffer_Type; Output : out Buffer_Type);
The purpose of this procedure is to sort the Input buffer, putting the sorted result into the Output buffer. The input buffer cannot be modified. The compiler enforces this: since Input is an in parameter, it will be treated as a constant by the compiler.
There are many ways to implement this procedure, but for our purposes you should copy characters from the input buffer to the output buffer, one at a time, inserting them into the proper spot as you go. As characters are inserted into the output buffer, some of the existing characters will need to be shifted down, and the last character in the output buffer will "fall off the end." At the end of this process, none of the original characters in Output (which are treated as uninitialized data when the procedure starts anyway) will remain. This is not the most efficient way to write the procedure, but it leads to some interesting analysis issues that we will discuss.
Proceed as follows:
Write the body of Immutable_Sort so that it appears to work correctly. Don't worry about defining any aspects such as a pre- and postconditions. You might want to write a test program to build confidence that your code works.
SPARK will assume the output depends on the input, which is true in this case so you don't need to add a Depends aspect. However, you should run the SPARK tool to "examine" your code for violations of SPARK requirements and to check the data and information flow.
Write a postcondition that states that every character in the final output buffer exists in the input buffer. Use the SPARK tools to prove this condition.
Enhance the postcondition above to also state that every character in the input buffer exists in the final output buffer. Use the SPARK tools to prove this condition. Does this prove that the output is a permutation of the input? (Hint: no).
Enhance the postcondition again to also state that the output is in sorted order. Use the SPARK tools to prove this condition. Does this prove the procedure works? (Hint: no).
Last Revised: 2019-08-02
© Copyright 2019 by Peter C. Chapin