K-user mailing list

[Björn Engelmann <bjoern.engelmann AT uni-oldenburg.de>]

Hi,

I was curious about this new program verification feature and wanted to
try it, but stumbled upon the following situation:

1) I took the kernelc-bubble-sort example from the samples directory,
kompiled it for the java backend and kran it with --prove
bubble_sort_spec.k and all the options listed in the config.xml file in
that directory. => everything seemed to work fine and I got

true
[]
true

Which I interpreted as "verification successful, specification holds."

2) Curious as I am, I replaced the postcondition in bubble_sort_spec.k
by "false", expecting things to fail, but when I kran with --prove
again, it again replied

true
[]
true

3) When I am not mistaken, then under the partial correctness
interpretation, non-terminating programs are allowed to have a {false}
postcondition, so I kran bubble-sort.c without the --prove option, and
got a final state, which AFAIK means it terminated...

Now I am pretty much stuck as I don't know if
a) the initial specification does not hold and the "true [] true"
actually indicates just that or
b) my postcondition "false" does not mean what I intended it to mean or
c) there is a bug in the verifier allowing it to derive a false
postcondition for a terminating program.

I packaged up all files necessary (case.tar.bz2), along with a
shell-script (run-prover.sh) that reproduces the case on my machine.

kompile --version output:

K framework version 3.5.1
Git revision: c41270a
Git branch: UNKNOWN
Build date: Thu Jan 29 23:40:05 CET 2015

could someone either:
- explain what I misunderstood or
- see if there is a bug, please?

Thanks in advance,
  Björn Engelmann

Attachment: case.tar.bz2
Description: Binary data

Attachment: 0x21A81FE2.asc
Description: application/pgp-keys

Attachment: signature.asc
Description: OpenPGP digital signature