K-user mailing list

[Robby Findler <robby AT eecs.northwestern.edu>]

Hi all: I'm having trouble understanding a K program's behavior and I wondered if I could get some help.

Here's the program:

module IMP

  syntax AExp ::= Int 

                | "(" AExp ")"    [bracket]

                | AExp "/" AExp   [seqstrict, left]

  syntax BExp ::= Bool

                | "(" BExp ")"    [bracket]

                | AExp "<=" AExp  [seqstrict]

                > BExp "and" BExp [seqstrict]

  syntax KResult ::= Bool | Int 

           

  rule <k> I1:Int / 0 ...</k> => <k> "div0" </k>

  rule I1:Int <= I2:Int => I1 <=Int I2        

  rule true and B:BExp => B

  rule false and _ => false

endmodule

and here's the IMP program I run:

   false and (1/0 <= 3)

I would have expected it to produce two out comes ("div0" and false) because of the seqstrict annotation on the "and" production in the grammar. Specifically, I thought I'd get a heating/cooling rule that would apply to the program above that would move the (1/0 <= 3) _expression_ to the front of the K cell, and the the 1/0 would move to the front and then I'd get the div0 result. But instead I get this:

$ ../k/bin/krun --do-search --maude-cmd search x.impSearch results:

Solution 1, state 0:

<k>

 false 

</k>

I do see that if I remove the short-circuiting 'and' rule that I get the div0, but I cannot seem to get them both at once.

tia,

Robby