K-user mailing list

[<jpkratos AT gmail.com>]

Hello everyone, I'm interested in realize some model checking and reachability
analysis over an small language I defined using K. However, I haven't found
enough information on the K tutorials about this topic and the only resources
I've got that are near this topic are the JavaScript and C definition
available online.

I also found the article available at
https://runtimeverification.com/blog/k-framework-an-overview/ and tried the
example exposed here in the language IMP, that verifies the program sum.imp,
with no luck since the krun --prove sum-spec.k sum.imp program throws the
following error:

[Error] Critical: Parse error: Syntax error near unexpected character ' '
        Source(X:\gitProjects\KFramework\k-distribution-3.6\k\tutorial\1_k
\2_imp\lesson_5\.\sum-spec.k)
        Location(6,24,6,24)

The sum-spec.k file content is:

require "imp.k"

module SUM-SPEC
    imports imp

    rule
  <k>
    while (!(n <= 0)) {
      sum = sum + n;
      n = n + -1;
    }
    =>
    .
  ...</k>
  <state>...
    n |-> (N:Int => 0)
    sum |-> (S:Int => S +Int ((N +Int 1) *Int N /Int 2))
  ...</state>
  requires N >=Int 0

endmodule

The sum.imp program runs fine when run with krun.
I'm using the 3.4 version of K.

Any ideas of what I'm missing? Thanks in advance!