K-user mailing list

[Christos Kloukinas <c.kloukinas AT gmail.com>]

Hi, no idea really but I see the error message mentioning distribution 
3.6 and you state at the end that you've got 3.4?
Best,
Chris
On 18/01/2019 00:21, 
jpkratos AT gmail.com
 wrote:
> 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!