>why would the formal verification be any more correct than the program it is verifying?

It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result - especially in the most common settings targeted by verification, which is to say imperative, stateful programs or algortihms with a high degree of non-obvious optimisations. The simplest example is a sorting algorithm, which normally has a trivial spec but a non-trivial state at each step.

Interestingly, some specs are actually programs themselves, as has also been true for many on-paper specs which are actually reference implementations. Research using programs-as-specs is still pretty valuable, since in some domains a simpler program is actually the right and useful way to talk about a messier one.

▲ inigyou 2 hours ago | parent | next [-]

You know, the last time someone brought up formal verification of sorting I said what the trivial spec was, and then someone else pointed out why it's actually completely wrong.

So for pedagogical purposes, can you tell us what you think the trivial spec is?

▲ pastel8739 an hour ago | parent | next [-]

Ok, I’ll bite, why is this wrong?

For a list of items I and an operator LEQ which returns bool for any pair of items in I, SORT() returns a list S such that:

1. Every item in I is present exactly once in S

2. For each consecutive pair of items (S_i, S_j) in S, LEQ(S_i, S_j) is true.

▲ inigyou an hour ago | parent [-]

SORT(1,2,3,4,5,5,6) = 1,2,3,4,5,6

▲ defrost an hour ago | parent [-]

I'm sorry, do all 5's look the same to you!! /s

aka, one item in I is missing in your output.

▲ inigyou an hour ago | parent | next [-]

No, if it had one more 5 it would violate your specification that every time must occur exactly once.

Also, SORT(1,2,3,4) = 1,2,3,4,7

▲ defrost an hour ago | parent [-]

Not my specification (drive by third party)

but I do take the view that ( 1, 2, 3, 4, 5, 5, 6 ) is a list of seven values (perhaps the number of dollars in the pockets of seven distinct unique people) and when sorted the output should also have seven items that correspond to the seven input items.

> Also ...

Yeah, that needs tightening up by pastel8739

▲ Jtsummers 44 minutes ago | parent | next [-]

You need a way to differentiate the two 5s, that isn't present. If you had a list like:

  L = [(5,foo), (2,bar), (2,baz),...]

And did a:

  SORT(L, key=first) # or however it'd be specified

Then the duplicate 2s would be fine, because they're no longer duplicates, only duplicate keys. But it would still fail if (2,baz) showed up twice in the source and destination even though we've asked for SORT, not UNIQSORT.

	▲	defrost 12 minutes ago \| parent \| next [-]
		More seriously, > You need a way to differentiate the two 5s As there's no unique filtering or other reduction going on here, there's a permutation chain from input to output.
	▲	defrost 28 minutes ago \| parent \| prev [-]
		In the cases of `SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 ) and SORT ( 3, 2, 5, 5 ) ->> ( 2, 3, 5, 5 )` one or both of those might be incorrect ? ( I'm teasing, perhaps )

▲ inigyou 32 minutes ago | parent | prev [-]

The specification said

    Every item in I is present exactly once in S

5 is an item in I, and it is present exactly once in S.

▲

defrost 26 minutes ago | parent [-]

and 5 is another item in I, and it's not present in S.

▲

inigyou 22 minutes ago | parent [-]

Yes it is, it's right there, between the 4 and the 6.

	▲	defrost 11 minutes ago \| parent [-]
		That's not the same one - track the permutation chain.

▲ Jtsummers an hour ago | parent | prev [-]

> I'm sorry, do all 5's look the same to you!! /s

You have that /s tag, but this is actually the problem with pastel8739's spec as written.

>> 1. Every item in I is present exactly once in S

This actually does require inigyou's example to be the result of calling SORT when you cannot distinguish repeated items from each other.

  SORT([1,1]) => [1,1]

The item 1 (which one? doesn't matter, they both do but we only need one to fail the post-condition to invalidate the result) in the source list has a count of 2 in the destination list, so this is an invalid result by the supplied spec.

pastel8739's spec also doesn't exclude the possibility of inserting new values (so long as they aren't duplicates of items in the source list).

▲ edflsafoiewq 41 minutes ago | parent | prev [-]

1. The output is a permutation of the input.

2. If the comparison implements a strict total order, the output is sorted according to it.

	▲	Veserv 2 minutes ago \| parent \| next [-]
		You are correct. However, that specification is not trivial. Almost nobody correctly articulates property 1 when first encountering the problem if they do not already know the answer or are already aware it is a trick question (and even then most software developers still fail). Furthermore, that also sidesteps the problem of formally specifying what a permutation is. Unless you have a grab bag of already proven powerful theorems, the author is most likely also going to make a error doing that as well even if we start at a proof abstraction level comparable to normal programming. Reality is that trivial problems admit trivially wrong specifications exceedingly easily. There is little reason to assume that much more complicated problems that are hard to even articulate will magically support obviously correct specifications that are simpler and more understandable than the code.
	▲	esafak 6 minutes ago \| parent \| prev [-]
		See how easy it is once you have right terms ;)

▲ makeitdouble 4 hours ago | parent | prev | next [-]

> It is quite believable that it's easier to describe what a program should result in versus actually programming it to produce that result

This is obvious for the central cases of a program. It becomes less and less true when going toward the edge cases, especially for a wide array of input.

Complex specs becoming programs is IMHO the direct effect of that (defining what we want is just that burdensome, and special cases we haven't though of will still have a coherent definition in the spec), and we fall back to the base "is this spec even correct" issue the parent points out.

▲ Veserv 3 hours ago | parent | prev [-]

Huh? Sorting does not have a trivial specification. In fact, it is usually used as the first example of how easy it is to make specification errors because it seems trivial, but is actually not.

	▲	inigyou 2 hours ago \| parent \| next [-]
		The trivial sorting spec is actually very useful, it's just not complete. While knowing that your sorting program meets the complete spec proves it works correctly, if you wrote it intending to be a sort algorithm, and you have proven it meets the trivial spec, and you have a few unit tests, that's still very good-but-not-foolproof evidence it's correct.
	▲	pastel8739 an hour ago \| parent \| prev [-]
		do you have a reference to anywhere that discusses this further? It seems pretty trivial to me