[SAL] A question when using SAL
harryh23 at hotmail.com
Sun Jun 18 14:02:35 PDT 2006
Thanks for information. I modified the program and it is on below:
simple1: CONTEXT =
process: MODULE =
OUTPUT i: [0..100] -- modified (1)
LOCAL high: BOOLEAN -- modified (2)
DEFINITION high = i > 100 -- modified (3)
i = 1
i<100 --> i' = i+1;
th1: THEOREM process |- F(i=110); -- modified (4)
(1), (2), (3), (4) are the modified code. This code passed the compiler. But
I have some two issues do not understand. First, for the modification (4),
it should not hold because in the transition, the loop stops incrementing i
by 1 if i reach 100. But when I used "sal-smc simple1 th1", it still said
proved. Second, I saw there is way to define invariant in the "DEFINITION",
so I define a invariant in modification (3). But why the using of "sal-smc
simple1 th1" still said it is proved ?
Can someone gives me hints ? Thanks.
>From: Ashish Tiwari <tiwari at csl.sri.com>
>To: harry huang <harryh23 at hotmail.com>
>CC: sal at csl.sri.com
>Subject: Re: [SAL] A question when using SAL
>Date: Sat, 17 Jun 2006 16:51:55 -0700 (PDT)
>The type "INTEGER" is not bounded; it has infinitely
>You will have to replace it by a finite subrange type
>(e.g. [0..100]) for sal-smc to work on this example.
>Hope this helps,
>On Sat, 17 Jun 2006, harry huang wrote:
>>I have a question when using SAL.
>>I want to express a process doing in below after try to verify that
>>eventually that i == 100
>>for (i = 1; i<100; i++);
>>So , I made a SAL program in below
>>simple1: CONTEXT =
>>process: MODULE =
>> OUTPUT i: INTEGER
>> i = 1
>> i<100 --> i' = i+1;
>>th1: THEOREM process |- F(i=100);
>>But when I used the command "sal-smc simple1 th1", it gave me the error
>>Error: [Context: simple1, line(6), column(16)]: Finite type representation
>>cannot be generated, type is not finite.
>>Reason: [Context: prelude, line(189), column(20)]: Type is not a bounded
>>subtype of integer, or it was not possible to determine the bound.
>>Can someone give me some hints ? Thanks.
More information about the SAL