laurayuwen

Hi, we usually recommend people who want to start using K to have a look at K tutorial http://www.kframework.org/index.php/K_Tutorial

Sorry, we haven't documented everything. You can find some examples, such as verifying some bst properties, in https://github.com/kframework/java-semantics, in src/verification

Could you try this? https://github.com/kframework/k/tree/javaCompatible

Yes, it can take half an hour or more. If your system get hanged, I am afraid so. On 19 January 2016 at 08:41, 20harshita [email protected] wrote: > after runing...

Looks nice! If we have a mechanism to produce AST from narrowing path (maude can already show the path), `mod GRAMMAR` can be further simplified to have rules look like...

@yilongli Yes, you are right. I didn't think of that. Timeout is a rather clear issue, we can have better output message.

This says the kompile command cannot be found, Have you add k's bin to path? Kjkompile is a wrapper that wraps a couple k command together, and the error reported...