I spent some time using systems that seem to do what you are trying to do. One of those is Specware (http://www.specware.org/ http://www.specware.org/). When I

I spent some time using systems that seem to do what you are trying to do. One of those is Specware (http://www.specware.org/ http://www.specware.org/). When I used Specware their tutorial had a sorting example just like yours but it seems in their latest tutorial they have a different example. My experience is that that those systems are very hard to use and very limited in their capabilities.