Frama-C-discuss mailing list archives

This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Jessie sort specification

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