V. P. Koryavtsev, I. A. Kudryavtseva
Price: 50 руб.
The definitions of a “certified programme” and “certified programming” are formulated
in the paper. The authors build the architecture of a certified programme according
to aforementioned definitions with the emphasis on learning how to write a certified
program using the Coq system and give an example of this programme. The authors also provide the certified programming syllabus, problem types, and examples of utilities for writing and verifying certified programmes.
Key words: valid programme, programme specification, programme verification,
certified programme, proving-oriented programming, certified programming.
References
1. Agafonov V. N. Spetsifikatsiya programm: ponyatiynye sredstva i ikh organizatsiya. Novosibirsk: Nauka, 1987. 240 s.
2. GOST R ISO/MEK 9126-93. Informatsionnaya tekhnologiya. Otsenka programmnoy produktsii. Kharakteristika kachestva i rukovodstva po ikh primeneniyu. 1994; 2004 // Elektronnyi fond pravovoy i normativno-tekhnicheskoy dokumentatsii. URL: http://docs.cntd.ru/document/1200009076 (data obrashcheniya: 02.10.2017).
3. GOST R ISO 9000-2008. Natsional’nyi standart Rossiyskoy Federatsii sistemy menedzhmenta kachestva. Osnovnye polozheniya i slovar’. 2009 // Elektronnyi fond pravovoy i normativno-tekhnicheskoy dokumentatsii. URL: http://docs.cntd.ru/document/1200068733 (data obrashcheniya: 02.10.2017).
4. GOST ISO 9000-2011. Mezhgosudarstvennyi standart sistemy menedzhmenta kachestva. Osnovnye polozheniya i slovar’. 2013 // Elektronnyi fond pravovoy i normativno-tekhnicheskoy dokumentatsii. URL:
http://docs.cntd.ru/document/ 1200093424 (data obrashcheniya: 02.10.2017).
5. Dokazatel’noe programmirovanie // Uchebno-metodicheskiy kompleks «Elektronnyi uchebnik». URL: http://main.tpkelbook.com/pre020.php?lc=0&pc=2&spn=Dokazatel’noe%20programmirovanie&sid
=19&qsid=19&apl=5&lst=0&stid=&grupID= (data obrashcheniya: 18.10.2017).
6. Kaufman V. Sh. Yazyki programmirovaniya. Kontseptsii i printsipy. M.: Radio i svyaz’, 1993. 432 s.
7. Krupskiy V. N., Kuznetsov S. L. Praktikum po matematicheskoy logike. Coq // MGU im. M. V. Lomonosova, 2013. 79 s. URL: http://lpcs.math.msu.su/~krupski/download/coq_pract.pdf (data obrashcheniya: 18.10.2017).
8. Nepeyvoda N. N. Prikladnaya logika. Izhevsk: Izd-vo Udmurtskogo un-ta, 1997. 385 s.; Novosibirsk: Izd-vo Novosibirskogo un-ta, 2000. 521 s.
9. Pro testing.RU // Home Comics Posts Publications Talks Misc About RSS. URL: http://protesting.ru (data obrashcheniya: 02.10.2017).
10. Razrabotka tekhnologii verifikatsii upravlyayushchikh programm so slozhnym povedeniem, postroennykh na osnove avtomatnogo podkhoda / Ruk.: A. A. Shalyto, isp. A. S. Krass. // Otchet o patentnykh issledovaniyakh, № 2007.08.31-01 ot 31.08.2007. 38 s. URL: http://is.ifmo.ru/verification/ _2007_01_patent-verification.pdf (data obrashcheniya: 02.10.2017).
11. Federal’nyi zakon RF. O tekhnicheskom regulirovanii (s izmeneniyami na 29 iyulya 2017 goda) // Elektronnyi fond pravovoy i normativno-tekhnicheskoy dokumentatsii. URL: http://docs.cntd.ru/document/901836556 (data obrashcheniya: 02.10.2017).
12. Chlipala A. Certified Programming with Dependent Types.: MIT Press, 2017.
