An example of a constructive specification of a queue, preliminary report, appendix B

An example is presented of the constructive specification of a queue which is done in the style of (Jones 80) using the Vienna Development Method. The basic approach is that of data type refinement. The techniques used are not restricted to those used by Jones, particularly with respect to the method for proving properties of the retrieve function for linked lists, however the notation is consistent with his.