--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on June 2009 ---
Hi, >We were trying to prove the postcondition without "advanced algebraic >modeling". >The reason for this attempt is a customer that feels a bit overwhelmed >by inductive definitions. > >Do you think it is possible that Jessie can prove a sort algorithm >that has not been "inductively specified"? I am not sure this is an answer to your question, but how about the following partial specification for a sort function: * every element in the result array appears somewhere in the argument array. * every element in the argument array appears somewhere in the result array. * the result array is ordered. This specification is partial, but it's still pretty good. It also seems easier to understand (I almost typed it in ACSL, but I decided I'd leave you the fun of it, and save my reputation). You can change it in a complete specification that may feel less complicated than the definition you are referring to by changing the "every element" parts into "the number of occurrences of ...". You only need one of the first two propositions if you do that, I do not know which one is easier to prove nor how that compares to the inductive definition that you are trying to avoid. Best regards, Pascal