b'\n_START_ARTICLE_\nATS (llenguatge de programaci\xc3\xb3)\n_START_SECTION_\nHist\xc3\xb2ria\n_START_PARAGRAPH_\nATS deriva d\'una versi\xc3\xb3 anterior anomenada DML \xc3\xb3 Dependent ML_NEWLINE_Tamb\xc3\xa9 hi ha antecedents en el "De Caml" versi\xc3\xb3 de Caml Light amb "tipus dependents de valors" del mateix autor.\n_START_SECTION_\nEfici\xc3\xa8ncia\n_START_PARAGRAPH_\nSegons l\'autor Hongwei Xi la seva efici\xc3\xa8ncia \xc3\xa9s deguda a la representaci\xc3\xb3 de dades i optimitzaci\xc3\xb3 de la recursivitat final. Els tipus s\xc3\xb3n principalment per a assegurar la correcci\xc3\xb3.\n_START_SECTION_\naplicaci\xc3\xb3\n_START_PARAGRAPH_\nL\'avaluaci\xc3\xb3 de fact1(n-1) torna un parell ( predicat_n_menys_1 | resultat_n_menys_1) que es fa servir en el c\xc3\xa0lcul de fact1(n)._NEWLINE_// fitxer fact1.dats (1a. part)(* [FACT (n, r)] \xc3\xa9s una proposici\xc3\xb3 certa si i nom\xc3\xa9s si [fact (n) = r] [MUL( n, m, prod)] \xc3\xa9s una proposici\xc3\xb3 certa si i nom\xc3\xa9s si [n * m = prod] {...} indica quantificaci\xc3\xb3 universal [...] indica quantificaci\xc3\xb3 existencial (...) tuples a (... | ...), | separa prova i valor les variables amb prefix pf_ responen a l\'abreviaci\xc3\xb3  de l\'angl\xc3\xa8s "proof" (cat: prova (predicat en aquest cas)) fact(0) = 1 ; r1 = fact(n-1); r = fact(n) = n * r1; per a n > 0*)dataprop FACT (int, int) =_NEWLINE_ | FACTbas (0, 1) // cas base: (fact(0) = 1)_NEWLINE_ | {n:int | n > 0} {r,r1:int} FACTind (n, r) of (FACT (n-1, r1), MUL (n, r1, r)) // cas inductiu _NEWLINE__NEWLINE_// fact1 implementa la funci\xc3\xb3 factorial sense recursivitat final// int(n) o tamb\xc3\xa9 \'\'int n\'\' \xc3\xa9s el tipus enter monovalor de valor nfun fact1 {n:nat} .< n >. (num: int(n))_NEWLINE_ (* {n:nat} univers .< n >. m\xc3\xa8trica (num: int(n)) par\xc3\xa0metre i tipus *)_NEWLINE_ : [r:int] (FACT (n, r) | int(r)) // tipus del resultat, retorna un parell (predicat | valor)_NEWLINE_ =_NEWLINE_ if num > 0 then_NEWLINE_ let_NEWLINE_ val (prova_fact_n_menys_1 | r1) = fact1 (num-1) // prova_fact_n_menys_1 = FACT( num-1, r1) _NEWLINE_ val (prova_mul | r) = num imul2 r1 // prova_mul = MUL( num, r1, r)_NEWLINE_ in_NEWLINE_ (FACTind (prova_fact_n_menys_1, prova_mul) | r)_NEWLINE_ end_NEWLINE_ else (FACTbas () | 1)_NEWLINE_rutines i principal:_NEWLINE_// fitxer fact1.dats (2a. part)// \'\'fn\'\' introdueix funci\xc3\xb3 no recursiva; \'\'fun\'\' introdueix funci\xc3\xb3 recursiva (admet m\xc3\xa8trica)fn abs {n:int} (num: int(n)): [r: nat] int(r) =_NEWLINE_ if num >= 0 then num else ~numimplement main (argc, argv) : void =_NEWLINE_ if (argc <> 2) then _NEWLINE_ printf ("us: %s 99 (un argument i prou)\\n", @(argv.[0]))_NEWLINE_ else let_NEWLINE_ val num = int1_of argv.[1]_NEWLINE_ val num_nat = abs num_NEWLINE_ val (prova_fact_n | res) = fact1 num_nat_NEWLINE_ in_NEWLINE_ printf ("factorial de %i = %i\\n", @(num_nat, res))_NEWLINE_ end_NEWLINE_Compilaci\xc3\xb3 (compila mitjan\xc3\xa7ant gcc, sense recollidor de mem\xc3\xb2ria brossa excepte si s\'especifica expl\xc3\xadcitament amb l\'opci\xc3\xb3 -D_ATS_GCATS_NEWLINE__NEWLINE_atscc fact1.dats -o fact1_NEWLINE_./fact1 4_NEWLINE_d\xc3\xb3na el resultat esperat_NEWLINE__NEWLINE_factorial de 4 = 24\n_START_SECTION_\nDetalls comuns\n_START_PARAGRAPH_\nATS utilitza quantificadors universals i existencials aix\xc3\xad com tipus d\'un sol valor (anomenats tipus singleton)_NEWLINE__NEWLINE_ {...} quantificador universal_NEWLINE_ [...] quantificador existencial_NEWLINE_ {n:nat | n > 2} univers o domini (anomenat \'\'sort\'\') dels naturals majors que 2_NEWLINE_ {n:nat} int(n) tipus de sencer corresponent a l\'univers de n_NEWLINE_ {n:nat} int n notaci\xc3\xb3 equivalent a l\'anterior_NEWLINE_ _NEWLINE_ // per exemple a la funci\xc3\xb3 abs: _NEWLINE_ // \xe2\x88\x80 n de l\'univers dels sencers, \xe2\x88\x83 r de l\'univers dels naturals_NEWLINE__NEWLINE_ fn abs {n:int} (num: int(n)): [r: nat] int(r) =_NEWLINE_ if num >= 0 then num else ~num\n_START_SECTION_\nsorts\n_START_PARAGRAPH_\nUnivers o domini de valors_NEWLINE__NEWLINE__NEWLINE_ sortdef nat = {a:int | a >= 0} // predefinit al \'\'Prelude\'\'_NEWLINE_ sortdef positius = {n:nat | n >= 1}_NEWLINE_ sortdef positius_entre_deu_i_20 = {n:positius | n >= 10 && n <= 20} _NEWLINE__NEWLINE_\xc3\xbas en especificaci\xc3\xb3 de par\xc3\xa0metre:tipus_NEWLINE__NEWLINE_{n:positius_entre_deu_i_20} num: int(n)_NEWLINE_algebraics_NEWLINE__NEWLINE_datasort alg_nats = Zero of () | Succ of alg_nats\n_START_SECTION_\ndatatypes a la ML\n_START_PARAGRAPH_\ndatatype diaFeiner = Dl | Dt | Dm | Dj | Dv_NEWLINE_llistes:_NEWLINE__NEWLINE_datatype list0 (a:t@ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)\n_START_SECTION_\nM\xc3\xb2duls\n_START_PARAGRAPH_\nCodi dels m\xc3\xb2duls:_NEWLINE__NEWLINE_ staload "foo.sats" // \'\'obre\'\'/importa el m\xc3\xb2dul foo.sats incorporant els identificadors a l\'espai de noms actual_NEWLINE__NEWLINE_ staload F "foo.sats" // requereix qualificador com ara $F.bar_NEWLINE__NEWLINE_ dynload "foo.dats" // carrega el m\xc3\xb2dul din\xc3\xa0micament (en temps d\'execuci\xc3\xb3)'