Formální verifikace podle typu na rozsah

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Formální verifikace podle typu na rozsah
« kdy: 01. 05. 2018, 00:57:43 »
Zdravím.

Mějme takovouto funkci v blíže neurčeném jazyku podobném haskellu:
Kód: [Vybrat]
fn s : String 0 40 -> String 4 20 =
    if (Str.len s) < 2 then
        "default"
    else
        Str.sub s 20
Čtěte to prosím jako "funkce fn má jeden parametr typu String který je minimálně nula znaků dlouhý, a maximálně 40; a vrací String, který je minimálně čtyři znaky dlouhý a maximálně 20.

A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?

(Tak jasně, můžu na to pustit testy, ale já bych rád zůstal jen u typů a formální verifikace.)

Díky.


Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Formální verifikace podle typu na rozsah
« Odpověď #1 kdy: 01. 05. 2018, 01:19:11 »
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #2 kdy: 01. 05. 2018, 01:41:41 »
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Formální verifikace podle typu na rozsah
« Odpověď #3 kdy: 01. 05. 2018, 04:29:20 »
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.

Radek Miček

Re:Formální verifikace podle typu na rozsah
« Odpověď #4 kdy: 01. 05. 2018, 09:30:50 »
A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?

Např. když si délkově omezený řetězec zadefinuji jako

Kód: [Vybrat]
data BString : Nat -> Nat -> Type where
  MkBString : (a : Nat) -> (b : Nat) -> (s : String) -> (LTE a (length s)) -> (LTE (length s) b) -> BString a b

tak abych do něj zabalil "default", musím psát něco jako

Kód: [Vybrat]
d : BString 4 20
d = MkBString 4 20 "default" (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))

kde poslední dva termy typů (LTE 4 7) a (LTE 7 20) jsou důkazy, že 4 <= 7 a 7 <= 20. V tomto případě by stačilo místo nich dát podtržítko a kompilátor je vymyslí sám. Nicméně i ve vaší funkci by bylo třeba dát důkazy, že nerovnosti platí - bez toho by se program nepřeložil.


BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #5 kdy: 01. 05. 2018, 12:25:14 »
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.
Díky.
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #6 kdy: 01. 05. 2018, 12:29:12 »
A mě by zajímalo, jak má nebohý typový systém odvodit, že ta funkce je špatně?

Např. když si délkově omezený řetězec zadefinuji jako

Kód: [Vybrat]
data BString : Nat -> Nat -> Type where
  MkBString : (a : Nat) -> (b : Nat) -> (s : String) -> (LTE a (length s)) -> (LTE (length s) b) -> BString a b

tak abych do něj zabalil "default", musím psát něco jako

Kód: [Vybrat]
d : BString 4 20
d = MkBString 4 20 "default" (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))) (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc (LTESucc LTEZero)))))))

kde poslední dva termy typů (LTE 4 7) a (LTE 7 20) jsou důkazy, že 4 <= 7 a 7 <= 20. V tomto případě by stačilo místo nich dát podtržítko a kompilátor je vymyslí sám. Nicméně i ve vaší funkci by bylo třeba dát důkazy, že nerovnosti platí - bez toho by se program nepřeložil.

Trochu jsem se v tom ztratil. Je to odpověď, na to, jak zjistí, že výstup není správně (to není tak zajímavé), nebo to, jak zjistí, že ta větev else, přestože může vrátit výsledek neodpovídající požadovanému výstupu, tak vždy vrátí (vrátila by) správný výsledek, protože proběhne jen v těch případech (to mě zajímá).

Díky.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Formální verifikace podle typu na rozsah
« Odpověď #7 kdy: 01. 05. 2018, 18:42:12 »
To jsou závislostní typy, verifikace se dělá přes theorem proving (takže překlad programu někdy trvá hodiny). Viz například jazyk Idris.
Mohl by si prosím lidsky popsat princip, jak se ta verifikace dělá?
Jako normální typová analýza, akorát typové operátory (konstruktory) berou i hodnoty krom typů. Třeba append na řetězcích by měl typ "String n m -> String k l -> String (n+k) (m+l)", takže v rámci typové kontroly (tj. během překladu, ne až za běhu) se počítá, v tomto případě s přirozenými čísly. Musí se dávat pozor na subsumpci a varianci, třeba String n m je podtypem String k l, pokud n>=k & m<=l.
Díky.
Uniká mi v tvé odpovědi, jak ten systém pozná, že Str.sub s 20 ve větvi else vrátí vždy korektní minimální čtyři znaky. (Tedy v mém případě pozná, že nevrátí, a tudíž nahlásí chybu.)
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #8 kdy: 01. 05. 2018, 21:05:31 »
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Formální verifikace podle typu na rozsah
« Odpověď #9 kdy: 01. 05. 2018, 22:40:31 »
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #10 kdy: 01. 05. 2018, 22:57:33 »
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.

Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.

Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).

Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).

Idris

  • *****
  • 2 286
    • Zobrazit profil
    • E-mail
Re:Formální verifikace podle typu na rozsah
« Odpověď #11 kdy: 02. 05. 2018, 00:06:59 »
To Str.sub bude mít svůj návratový typ, a pokud ten není podtypem návratového typu té vnější funkce, překladač zařve.
Tak v tom případě to není odpověď na mou otázku :-)

Str.sub vrací String 0 ∞, zatímco fn vrací String 4 20. Takže mi to může vrátit dvouznakový řetězec, a to už je špatně.

A přesto očekávám, že (v případě, když bych tam neměl tu záměrnou chybu) mi to překladač označí za korektní.
No ale přece String 0 ∞ není podtypem String 4 20, tady je ta kontrola ještě přímočará. Možná teda nejspíš nechápu otázku. BTW to Str.sub by mělo mít návratový typ také závislostní podle vstupních parametrů, jinak by byla typová kontrola příliš restriktivní.

Počkej, počkej, mám pocit, že jsme se tu někdo z nás ztratil.

Str.sub má návratový typ String 0 ∞. Takže může vrátit dvouznakový řetězec. Vstupní argumenty jsou 20, což je ok na výstup, takže tento argument změní návratový typ na String 0 20. A dále String, jehož minimální velikost je určena tou kontrolou v if. Což je tedy defakto taky správně, a ta funkce bude pracovat korektně. A já se tedy táži, jak typový systém pozná, že díky podmínce if se z hodnoty String 0 20 stane hodnota typu String 2 20 (respektive String 4 20).

Zdůrazňuji, že já se táži na typový systém, který řeší mou úlohu. Netáži se jak fungují závislostní typy (i když zrovna třeba ony mohou řešit mou úlohu, a pak mě zajímá jak to řeší).
Jo, teď jsem se už definitivně ztratil já :( Co je myšleno tím "změnit návratový typ"?

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #12 kdy: 02. 05. 2018, 00:39:00 »
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.

andy

Re:Formální verifikace podle typu na rozsah
« Odpověď #13 kdy: 02. 05. 2018, 10:14:53 »
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).
Napsalo by se to takhle:
Kód: [Vybrat]
fn s : String 0 40 -> String 4 20 =
    case s `hasMinimumLen` 4 of
        Just sn -> Str.sub sn 20 -- sn ma tady typ (String 4 40)
        Nothing -> "default"
Ono dnešní jazyky (Java..) by to uměly odvodit i z té podmínky - třeba "null" to schopné odvodit je, ale takhle je to hezčí a explicitně.

BoneFlute

  • *****
  • 1 981
    • Zobrazit profil
Re:Formální verifikace podle typu na rozsah
« Odpověď #14 kdy: 02. 05. 2018, 10:37:44 »
Napsalo by se to takhle:
Kód: [Vybrat]
fn s : String 0 40 -> String 4 20 =
    case s `hasMinimumLen` 4 of
        Just sn -> Str.sub sn 20 -- sn ma tady typ (String 4 40)
        Nothing -> "default"
Ono dnešní jazyky (Java..) by to uměly odvodit i z té podmínky - třeba "null" to schopné odvodit je, ale takhle je to hezčí a explicitně.
Fikaný!