[SAL] A question when using SAL

[harry huang]

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
>>
>>
>