K-user mailing list

[Andrei Stefanescu <andreistef AT gmail.com>]

Hi Bjorn,

Thank you for you interest in K and Matching Logic. There are two separate issues.

1. The specification rule has the [trusted] tag, which means the verifier does not attempt to prove it, but may use it in proving other rules. I used that tag for debugging purposes, and I forgot to remove it. Thank you for noticing!

2. There was indeed a bug in the translation of the ensures clauses in internal data structures, which has been fixed in the meantime. I suggest you use the latest version of K. You can get it from github (https://github.com/kframework/k, the master branch) or from the download page (http://www.kframework.org/index.php/K_tool_binaries, under latest). Please let us know if you have any more questions.

Andrei

On Tue, Apr 28, 2015 at 8:51 AM, Björn Engelmann <bjoern.engelmann AT uni-oldenburg.de> wrote:

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



_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user