Formální verifikace podle typu na rozsah

[Honza]

Jo, teď jsem se už definitivně ztratil já Co je myšleno tím "změnit návratový typ"?

:-D

Představme si, že jsem typový systém, a mám ověřit, zda tato funkce je v pořádku:

Kód: [Vybrat]

fn s : String 0 40 -> String 4 20 =
    if (Str.len s) < 4 then
        "default"
    else
        Str.sub s 20
Kouknu, a vidím, že na vstupu může přijít řetězec, minimálně 0, maximálně 40. Na výstupu je minimálně 4, max 20.
Takže 13 znaků cajk. 20 znaků cajk. 30 znaků cajk (hrubou silou oříznu). Ale 2 znaky už jsou problém, na vstupu přijít mohou, a na výstupu nesmí.

Funkce Str.sub s 20 v daném kontextu znamená Str.sub (String 0 40) 20 -> String 0 20 protože podle druhého argumentu si mohu odvodit, že tedy nedostanu delší string jak 20znaků, ale jako první argument stále mohu dostat prázdný string. A tedy nevím, jak bych měl uvažovat (jako ten typový systém).

Tedy samozřejmě si takhle jen hraju. Nikdy jsem typový systém neimplementoval, a tak se zkouším vcítit do jeho uvažování :-) A pravděpodobně někde mám i nějaké ty díry v úvaze.

Tak to je fikaný, teď je uvedeno:

Kód: [Vybrat]

if (Str.len s) < 4 then
zatímco původně bylo:

Kód: [Vybrat]

if (Str.len s) < 2 then
Jak to tedy má být?

[Reklama]

[BoneFlute]

Tak to je fikaný, teď je uvedeno:

Kód: [Vybrat]

if (Str.len s) < 4 then
zatímco původně bylo:

Kód: [Vybrat]

if (Str.len s) < 2 then
Jak to tedy má být?

To je fuk, ne? Otázka zněla, jak má typový systém ověřit správnost. V původním by nahlásil chybu, v tom druhém, že je to v pořádku. Podstatné je, zda je schopen.