K-user mailing list

[Patrick Meredith <pmeredit AT gmail.com>]

One definite issue is bool is in your syntax, so false and _ can be applied before any heating or cooling ever occurs.

-Patrick

On Oct 2, 2012 10:20 PM, "Robby Findler" <robby AT eecs.northwestern.edu> wrote:

Yes, but the left is already a KResult so the heating (or is it
cooling?) rule should still fire. No?

Robby

On Tue, Oct 2, 2012 at 10:16 PM, Patrick Meredith <pmeredit AT gmail.com> wrote:
> Hi Robby,
>
> Replace seqstrict with strict.  Seqstrict is deterministic sequentially
> (left to right)
>
> -Patrick
>
> On Oct 2, 2012 7:12 PM, "Robby Findler" <robby AT eecs.northwestern.edu> wrote:
>>
>> 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
>>
>> _______________________________________________
>> k-user mailing list
>> k-user AT cs.uiuc.edu
>> http://lists.cs.uiuc.edu/mailman/listinfo/k-user
>>
>
_______________________________________________
k-user mailing list
k-user AT cs.uiuc.edu
http://lists.cs.uiuc.edu/mailman/listinfo/k-user