Real-time OS system state captured by ATS language (and questions)

[Kiwamu Okabe]

Hi all,

A real-time OS, ChibiOS/RT, has system state as following:

http://www.chibios.org/dokuwiki/doku.php?id=chibios:book:kernel#system_states

I wrote following code to capture the state by ATS statics:

https://github.com/fpiot/chibios-ats-2/blob/b1445489b6a3d55a4cf39e74770fdb50ffb71c57/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L65

which `chss(chss_thread)` means the system state "Thread".
And there are some utility functions:

https://github.com/fpiot/chibios-ats-2/blob/b1445489b6a3d55a4cf39e74770fdb50ffb71c57/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L84

And then I wrote following "ISR" function, that is type-checked:

```
extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"
implement tmrfunc (pss | p) = {
val () = chSysLockFromISR (pss | )
val () = chEvtBroadcastI (pss | inserted_event_p)
val () = chSysUnlockFromISR (pss | )
}
```

However the other function is not type-checked:

```extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"
implement tmrfunc (pss | p) = {
val () = chSysLockFromISR (pss | )
val () = if true then chEvtBroadcastI (pss | inserted_event_p)
val () = chSysUnlockFromISR (pss | )
}
```

```
$ patsopt -o build/obj/main.c -d main.dats
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): mismatch
of static terms (equal):
The actual term is: S2Eapp(S2Ecst(chss_ilock); )
The needed term is: S2Eapp(S2Ecst(chss_isr); )
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); ))
The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); ))
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3483(line=100, offs=65) -- 3483(line=100, offs=65): error(3): the
dynamic variable [pss$3868(-1)] is retained but with a type that fails
to merge.
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): mismatch
of static terms (equal):
The actual term is: S2Eapp(S2Ecst(chss_ilock); )
The needed term is: S2Eapp(S2Ecst(chss_isr); )
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); ))
The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); ))
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3443(line=100, offs=25) -- 3483(line=100, offs=65): error(3): the
dynamic variable [pss$3868(-1)] is retained but with a type that fails
to merge.
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): the
dynamic expression cannot be assigned the type [S2Eapp(S2Ecst(chss);
S2Eapp(S2Ecst(chss_ilock); ))].
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): mismatch
of static terms (equal):
The actual term is: S2Eapp(S2Ecst(chss_isr); )
The needed term is: S2Eapp(S2Ecst(chss_ilock); )
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
3512(line=101, offs=29) -- 3515(line=101, offs=32): error(3): mismatch
of static terms (tyleq):
The actual term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_isr); ))
The needed term is: S2Eapp(S2Ecst(chss); S2Eapp(S2Ecst(chss_ilock); ))
patsopt(TRANS3): there are [3] errors in total.
```

What happens? I think I miss-understand linear type...

Best regards,
--
Kiwamu Okabe at METASEPI DESIGN

[gmhwxi]

>>val () = if true then chEvtBroadcastI (pss | inserted_event_p)

The system does not know what type should be given to pss. You
need state type annotation:

https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!topic/ats-lang-users/WfatF27cyDc

if chEvtBroachcastI does not change the type of pss, you may just do

prval pss2 = pss
val () = if true then chEvtBroadcastI (pss2 | inserted_event_p)
...
prval () = (pss := pss2)

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Jun 12, 2016 at 9:38 PM, gmhwxi <gmh...@gmail.com> wrote:
>>>val () = if true then chEvtBroadcastI (pss | inserted_event_p)
>
> The system does not know what type should be given to pss. You
> need state type annotation:
>
> https://groups.google.com/forum/?utm_medium=email&utm_source=footer#!topic/ats-lang-users/WfatF27cyDc

Sorry. I can't imagine how to apply the state type annotation to my situation...
Could you show more detail in the example?

> if chEvtBroachcastI does not change the type of pss, you may just do
>
> prval pss2 = pss
> val () = if true then chEvtBroadcastI (pss2 | inserted_event_p)
> ...
> prval () = (pss := pss2)

Your code is type-checked.
However, why is renaming pss needed? I think simple renaming is not
hint for ATS2 compiler...

[Kiwamu Okabe]

On Mon, Jun 13, 2016 at 12:36 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
>> if chEvtBroachcastI does not change the type of pss, you may just do
>>
>> prval pss2 = pss
>> val () = if true then chEvtBroadcastI (pss2 | inserted_event_p)
>> ...
>> prval () = (pss := pss2)
>
> Your code is type-checked.
> However, why is renaming pss needed? I think simple renaming is not
> hint for ATS2 compiler...

More complex code is also type-checked... It's mysterious for me...

```
extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"
implement tmrfunc (pss | p) = {

val bbdp = $UN.cast{cPtr0(BaseBlockDevice)}(p)

val () = chSysLockFromISR (pss | )

val cnt = $extval(int, "cnt")
prval pss2 = pss
val () = if cnt > 0 then
if blkIsInserted (bbdp) then {
extvar "cnt" = cnt - 1
val cnt = $extval(int, "cnt")
val () = if cnt = 0 then chEvtBroadcastI (pss2 |
inserted_event_p)
} else {
extvar "cnt" = POLLING_INTERVAL
}
else if ~blkIsInserted(bbdp) then {
extvar "cnt" = POLLING_INTERVAL
val () = chEvtBroadcastI (pss2 | removed_event_p)
}
prval () = pss := pss2
val () = chVTSetI (tmr_p, MS2ST (POLLING_DELAY),
$UN.cast{vtfunc_t}(tmrfunc), bbdp)

val () = chSysUnlockFromISR (pss | )
}
```

[gmhwxi]

You need to the following annotation:

if :(pss: chss(chss_ilock)) =>

  true then chEvtBroadcastI (pss | inserted_event_p)

If no annotation is given, then the following default is assumed:

if :(pss: chss(chss_isr)) =>

  true then chEvtBroadcastI (pss | inserted_event_p)

This is due to 'pss' being originally given the type chss(chss_isr)

If you do:

prval pss2 = pss

then the 'original' type for pss2 is chss(chss_isr). So if you use
pss2, you do not need to provide an explicit state type annotation.

[Kiwamu Okabe]

Hi Hongwei,

On Mon, Jun 13, 2016 at 1:04 PM, gmhwxi <gmh...@gmail.com> wrote:
> You need to the following annotation:
>
> if :(pss: chss(chss_ilock)) =>
> true then chEvtBroadcastI (pss | inserted_event_p)
>
> If no annotation is given, then the following default is assumed:
>
> if :(pss: chss(chss_isr)) =>
> true then chEvtBroadcastI (pss | inserted_event_p)
>
> This is due to 'pss' being originally given the type chss(chss_isr)

Umm...
The `pss` is introduced as `chss(chss_isr)` at the `tmrfunc` function.
However the `chEvtBroadcastI` function doesn't know that it was
changed into `chss(chss_ilock)`?
If so, how does `chSysUnlockFromISR` function know the changing?

> If you do:
>
> prval pss2 = pss
>
> then the 'original' type for pss2 is chss(chss_isr). So if you use
> pss2, you do not need to provide an explicit state type annotation.

I think it makes sense.
Does it mean that 'initial' type of linear type is only used in if expression?

[Kiwamu Okabe]

Hi Hongwei,
I have more questions...

If `chEvtBroadcastI` should be only called from both S-Locked and
I-Locked state,
then the code is written with following:

```
datasort chss =
| chss_init | chss_thread | chss_irqsusp | chss_irqdisable |
chss_irqwait | chss_isr | chss_slock | chss_ilock
absvtype chss(s:chss)
vtypedef chss_anylock = [s:chss | s == chss_slock || s == chss_ilock] chss(s)

extern fun chEvtBroadcastI (!chss_anylock | cPtr0(event_source_t)):
void = "mac#"

extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"
implement tmrfunc (pss | p) = {
val () = chSysLockFromISR (pss | )

val () = chEvtBroadcastI (pss | removed_event_p)

val () = chSysUnlockFromISR (pss | )
}

extern fun tmr_init (!chss(chss_thread) | ptr): void = "mac#"
implement tmr_init (pss | p) = {
val () = chSysLock (pss | )
val () = chEvtBroadcastI (pss | removed_event_p)
val () = chSysUnlock (pss | )
}
```

But the code can't be type-checked:

```

patsopt -o build/obj/main.c -d main.dats
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:

3392(line=98, offs=28) -- 3415(line=98, offs=51): error(3): unsolved
constraint: C3NSTRprop(C3TKmain(); S2Eapp(S2Ecst(||);
S2Eapp(S2Ecst(==); S2EVar(4505->S2Eapp(S2Ecst(chss_ilock); )),
S2Eapp(S2Ecst(chss_slock); )), S2Eapp(S2Ecst(==);
S2EVar(4505->S2Eapp(S2Ecst(chss_ilock); )), S2Eapp(S2Ecst(chss_ilock);
))))
typechecking has failed: there are some unsolved constraints: please
inspect the above reported error message(s) for information.
exit(ATS): uncaught exception:
_2home_2kiwamu_2src_2ATS_2dPostiats_2src_2pats_error_2esats__FatalErrorExn(1025)
```

How to define linear type as `chss_anylock`?

[Hongwei Xi]

== is not defined for terms of datasort chss.

Don't define chss as a datasort. Try:

sortdef chss = int

#define chss_init 0

#define chss_ilock ...

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dkn15HFdDQ8zW9Yav3mqMk9hKJgc-333D2_U4byqx2qnw%40mail.gmail.com.

[gmhwxi]

Such use of initial types only involves if-expressions and case-expressions.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 3:04 PM, gmhwxi <gmh...@gmail.com> wrote:
> Such use of initial types only involves if-expressions and case-expressions.

Thanks. I think I understand it.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 1:23 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> == is not defined for terms of datasort chss.
>
> Don't define chss as a datasort. Try:
>
> sortdef chss = int
> #define chss_init 0
> #define chss_ilock ...

There are no method to introduce == operation over my datasort?
May I use `stacst` for it?

[gmhwxi]

You can introduce it, but the constraint solver does not understand it.

You need to introduce a dataprop:

dataprop EQCHSS(chss, chss) = EQCHSS of ()

But this is not easy to use. I think the easiest way is to define chss as int.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 1:23 PM, Hongwei Xi <gmh...@gmail.com> wrote:

> == is not defined for terms of datasort chss.
>
> Don't define chss as a datasort. Try:
>
> sortdef chss = int
> #define chss_init 0
> #define chss_ilock ...

It's type-checked.

Next, I would like to specify bound of sort `chss`.
However following code is not type-checked...

```
#define chss_init 0
#define chss_thread 1
#define chss_irqsusp 2
#define chss_irqdisable 3
#define chss_irqwait 4
#define chss_isr 5
#define chss_slock 6
#define chss_ilock 7
sortdef chss = { i:int | chss_init <= i; i <= chss_ilock }
absvtype chss(s:chss)
```

```
/home/kiwamu/src/chibios-ats-2/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats:
1952(line=74, offs=17) -- 1956(line=74, offs=21): error(2): the
identifier [chss] is expected to refer to a sort (instead of a subset
sort).
```

I found above style in ATS-Postiats-contrib.
The style can't be used with absvtype?

[Hongwei Xi]

chss is not a sort; it is a subset sort, which can not be

used to index a type. Try:

abstype chss(int)

praxi lemma_chss{n:int} (!chss(n)): [0 <= n; n <= 7] void

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnX68Ryu0SzSYuGRfj4xgMjr6OWXTGPndaLFXMFaL0Vbw%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 4:52 PM, gmhwxi <gmh...@gmail.com> wrote:
> You can introduce it, but the constraint solver does not understand it.
>
> You need to introduce a dataprop:
>
> dataprop EQCHSS(chss, chss) = EQCHSS of ()

I remember this pattern.
I should static function such like `fib_b` for this case?

http://ats-lang.sourceforge.net/EXAMPLE/EFFECTIVATS/PwTP-bool-vs-prop/main.html

> But this is not easy to use. I think the easiest way is to define chss as
> int.

O.K. I use this technique.

Thanks a lot,

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 4:55 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> chss is not a sort; it is a subset sort, which can not be
> used to index a type. Try:
>
> abstype chss(int)
>
> praxi lemma_chss{n:int} (!chss(n)): [0 <= n; n <= 7] void

I wrote following code:

```
#define chss_init 0
#define chss_ilock 7
absvtype chss(s:int)
extern praxi lemma_chss {n:int} (!chss(n)): [chss_init <= n; n <=
chss_ilock] void

fun foofunc (pss: !chss(10) | p: ptr): void = {
}
```

However it's type-checked...
How to avoid out of bound over the chss's int?
How to use `lemma_chss`?

[Hongwei Xi]

foofunc cannot be used as long as there is no way

to produce a value of the type chss(10).

You can form the type chss(10), but you should allow

a value of this type to be formed.

For instance, list(string, ~1) is a valid type but there is

no value of such a type.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dktUiGvAz40Qi_wDgoHazyYuSAKNMPXEUbS%3Dok7reDm%2BQ%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 15, 2016 at 10:19 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> foofunc cannot be used as long as there is no way
> to produce a value of the type chss(10).
>
> You can form the type chss(10), but you should allow
> a value of this type to be formed.
>
> For instance, list(string, ~1) is a valid type but there is
> no value of such a type.

Ah, I understand it.

However I can write following code:

```

extern praxi lemma_chss {n:int} (!chss(n)): [chss_init <= n; n <=
chss_ilock] void

fun barfunc (pss: !chss(10) | p: ptr): void = {}

extern fun foofunc (!chss(10) | ptr): void = "mac#"
implement foofunc (pss | p) = barfunc (pss | p)
```

The code is type-checked. And the `foofunc` function can be called
from C language.
What kind of error does it avoid?

[Hongwei Xi]

Typechecking can only be perfomed on ATS code.

If you call foofunc in C, there is no safety guarantee.

By the way, the example does not seem to be interesting because

barfunc cannot make any real use of pss.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dm%3D7BRN%3DN8EssYOtX5gH6E9ZbzO8im676zrcD5fVMjJkg%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Thu, Jun 16, 2016 at 12:58 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Typechecking can only be perfomed on ATS code.
>
> If you call foofunc in C, there is no safety guarantee.
>
> By the way, the example does not seem to be interesting because
> barfunc cannot make any real use of pss.

With your advice, my code is finally shaped as following:

https://github.com/fpiot/chibios-ats-2/blob/720847a31b9417ee267a34bf1746802e916ce03b/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L64

The code is type-checked, and captures system state for ch* function well.
However the code can't catch the error such like following:

```
extern fun chEvtObjectInit (!chss(10) | cPtr0(event_source_t)): void = "mac#"
```

I think ATS compiler can capture the error, if it supports int's
bounds depended by absvtype `chss`.
I hope the supporting becomes in future.

[Kiwamu Okabe]

Hi Hongwei,

I have the other question. Following code has `chVTSetI` function:

https://github.com/fpiot/chibios-ats-2/blob/720847a31b9417ee267a34bf1746802e916ce03b/demos/STM32/RT-STM32F746G-DISCOVERY-LWIP-FATFS-USB/main.dats#L84

The `chVTSetI` function has following type:

```
typedef vtfunc_t = ptr -> void
extern fun chVTSetI (!chss_iclass | cPtr0(virtual_timer_t), systime_t,
vtfunc_t, cPtr0(BaseBlockDevice)): void = "mac#"
```

The `chVTSetI` uses following `tmrfunc` as 3rd argument:

```

extern fun tmrfunc (!chss(chss_isr) | ptr): void = "mac#"

```

I would like to write the `chVTSetI` applying as following:

```
val () = chVTSetI (pss | tmr_p, MS2ST (POLLING_DELAY), tmrfunc, bbdp)
```

However the above code can't be shaped and I should use cast as following,
because `typedef` keyword can't define proof argument in the definition:

```
val () = chVTSetI (pss | tmr_p, MS2ST (POLLING_DELAY),
$UN.cast{vtfunc_t}(tmrfunc), bbdp)
```

Are there methods to define envless function typedef includes proof argument?

[gmhwxi]

What you need can be captured in ATS as follows:

(* ****** ****** *)
//
dataprop
chss_p(int) = {s:int | s <= 7} CHSS(s) of ()
//
(* ****** ****** *)
//
abst@ype event_source_t
//
extern
fun
chEvtObjectInit
  {s:int}
  (!chss(s), chss_p(s) | cPtr0(event_source_t)): void = "mac#"
//
(* ****** ****** *)

[gmhwxi]

I do not understand this question.

Why can't you define vtfunc_t as follows:

typedef
vtfunc_t = (!chss(chss_isr) | ptr) -> void

[Kiwamu Okabe]

Hi Hongwei,

On Sun, Jun 19, 2016 at 12:46 AM, gmhwxi <gmh...@gmail.com> wrote:
> Why can't you define vtfunc_t as follows:
>
> typedef
> vtfunc_t = (!chss(chss_isr) | ptr) -> void

Sorry... Today, I tried the above, and fixed it.
Thanks a lot,

[Kiwamu Okabe]

Hi Hongwei,
sorry for my waywardness.

On Sun, Jun 19, 2016 at 12:38 AM, gmhwxi <gmh...@gmail.com> wrote:
> What you need can be captured in ATS as follows:
>
> (* ****** ****** *)
> //
> dataprop
> chss_p(int) = {s:int | s <= 7} CHSS(s) of ()
> //
> (* ****** ****** *)
> //
> abst@ype event_source_t
> //
> extern
> fun
> chEvtObjectInit
> {s:int}
> (!chss(s), chss_p(s) | cPtr0(event_source_t)): void = "mac#"

I feed the using chss_p on every function is messy, because every
function needs two proof value...

Is it able to define `absvtype chss(s:int)` as private definition?
Please imagine following:

```
absvtype chss(s:int)
vtypedef chss_sinit = chss(chss_init)
vtypedef chss_any = [s:int | chss_init <= s; s <= chss_ilock] chss(s)
vtypedef chss_iclass = [s:int | s == chss_slock || s == chss_ilock] chss(s)
```

I think threre are no miss calling like `chss(10)` in application
code, if application programmer is
permitted to access `chss_sinit` / `chss_any` / `chss_iclass` and
prohibited to access `chss`,

[Hongwei Xi]

Or you can turn chss_p into a predicate:

stacst chss_p : (int) -> bool

Please take a look at the following code:

https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/test37.dats

There are many ways to address this issue. I don't feel it is worth the effort right now because

I don't see that anyone would be using a type like chss(10). If it turns out to be a real problem,

then you can always try to fix it later. Right now, this is all *imaginary*.

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6d%3D-v%3DO8YNpRCzz6pSG7ouTthQzbG9479hotsfoG35F-ZQ%40mail.gmail.com.

[Kiwamu Okabe]

Hi Hongwei,

On Wed, Jun 22, 2016 at 1:33 PM, Hongwei Xi <gmh...@gmail.com> wrote:
> Or you can turn chss_p into a predicate:
>
> stacst chss_p : (int) -> bool
>
> Please take a look at the following code:
>
> https://github.com/githwxi/ATS-Postiats-test/blob/master/contrib/hwxi/TEST30/test37.dats

Thanks. However this style needs injecting `{s:int | chss_p(s)}` into
every function...

> There are many ways to address this issue. I don't feel it is worth the
> effort right now because
> I don't see that anyone would be using a type like chss(10). If it turns out
> to be a real problem,
> then you can always try to fix it later. Right now, this is all *imaginary*.

Yes, you are right. This issue should occur when following:

* Application's function is introduced with a bad state number such
like `chss(10)`, and...
* All of system API called by the function has a bad state number.

Then I think that such error caused by bad state number is rare case.

Thanks,

[gmhwxi]

I want to use this occasion to mention a bit of experience I gathered in the past.
In my opinion, one should avoid trying to over-use types to capture programming errors.
It rarely pays if you try to target *imaginary* programming errors.

Many programmers think that program verification means to verify that a program is "100%"
correct (whatever it means). I thought likewise but I now think that program verification is just
some form of static debugging; it is meant to make a programmer more productive than if one
solely relies on dynamic debugging.

Too many programmers gave up ATS because they tried to do too much with types. Instead of
relying on typechecking to flush out potential bugs, they fought against typechecking futilely.

[Kiwamu Okabe]

Hi all,

On Sun, Jun 12, 2016 at 7:42 PM, Kiwamu Okabe <kiw...@debian.or.jp> wrote:
> A real-time OS, ChibiOS/RT, has system state as following:
>
> http://www.chibios.org/dokuwiki/doku.php?id=chibios:book:kernel#system_states
>
> I wrote following code to capture the state by ATS statics:

Today, I talk about this topic at ML study meeting.
The slide is found at following:

http://www.slideshare.net/master_q/realtime-os-system-state-captured-by-ats-language

Regards,

[Hongwei Xi]

Great!

Posted as a news piece at http://www.ats-lang.org/Community.html

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
Visit this group at https://groups.google.com/group/ats-lang-users.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CAEvX6dnSJp%2BsvQMESv19bVrFvZGUT_to7JrXOUwALC44F2Ya_A%40mail.gmail.com.