[SAL] A question when using SAL
harry huang
harryh23 at hotmail.com
Sun Jun 18 14:02:35 PDT 2006
Hi,
Thanks for information. I modified the program and it is on below:
====
simple1: CONTEXT =
BEGIN
process: MODULE =
BEGIN
OUTPUT i: [0..100] -- modified (1)
LOCAL high: BOOLEAN -- modified (2)
DEFINITION high = i > 100 -- modified (3)
INITIALIZATION
i = 1
TRANSITION
[
i<100 --> i' = i+1;
]
END;
th1: THEOREM process |- F(i=110); -- modified (4)
END
====
(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.
harry
>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
>many elements.
>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,
>-Ashish
>
>On Sat, 17 Jun 2006, harry huang wrote:
>
>>Hi,
>>
>>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
>>===
>>int i;
>>for (i = 1; i<100; i++);
>>===
>>
>>So , I made a SAL program in below
>>
>>====
>>simple1: CONTEXT =
>>BEGIN
>>
>>process: MODULE =
>> BEGIN
>> OUTPUT i: INTEGER
>> INITIALIZATION
>> i = 1
>> TRANSITION
>> [
>> increment:
>> i<100 --> i' = i+1;
>> ]
>> END;
>>
>>th1: THEOREM process |- F(i=100);
>>END
>>=====
>>
>>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.
>>
>>Harry
>>
>>
>
More information about the SAL
mailing list