Синтез программы

В информатике синтез программ — это задача создания программы , которая доказуемо высокого уровня удовлетворяет заданной формальной спецификации . В отличие от верификации программы , программу нужно сконструировать, а не дать; однако в обеих областях используются формальные методы доказательства, и обе включают подходы с разной степенью автоматизации. В отличие от методов автоматического программирования , спецификации при синтезе программ обычно представляют собой неалгоритмические утверждения в соответствующем логическом исчислении . ^[1]

Основное применение синтеза программ — избавить программиста от бремени написания правильного, эффективного кода, удовлетворяющего спецификации. Однако синтез программ также имеет приложения для супероптимизации и вывода инвариантов цикла . ^[2]

Происхождение [ править ]

Во время Летнего института символической логики в Корнельском университете в 1957 году Алонзо Чёрч определил проблему синтеза схемы на основе математических требований. ^[3]Несмотря на то, что эта работа относится только к схемам, а не к программам, эта работа считается одним из самых ранних описаний синтеза программ, и некоторые исследователи называют синтез программ «проблемой Черча». В 1960-х годах аналогичная идея «автоматического программиста» рассматривалась исследователями искусственного интеллекта. ^{[ нужна цитата ]}

С тех пор различные исследовательские сообщества рассматривали проблему синтеза программ. Известные работы включают теоретико-автоматный подход Бючи и Ландвебера 1969 года , ^[4]и работы Манны и Вальдингера (около 1980 г.). Развитие современных языков программирования высокого уровня также можно понимать как форму синтеза программ.

века События 21

В начале XXI века наблюдался всплеск практического интереса к идее синтеза программ в сообществе формальной верификации и смежных областях. Армандо Солар-Лезама показал, что можно кодировать задачи синтеза программ в булевой логике и использовать алгоритмы решения булевой задачи выполнимости для автоматического поиска программ. ^[5]

Синтаксис-ориентированный синтез [ править ]

В 2013 году исследователями из Университета Пенсильвании , Калифорнийского университета в Беркли и Массачусетского технологического института была предложена единая структура для решения задач синтеза программ под названием Синтаксис-ориентированный синтез (стилизованный SyGuS) . ^[6] Входные данные для алгоритма SyGuS состоят из логической спецификации и бесконтекстной грамматики выражений, ограничивающей синтаксис допустимых решений. ^[7] Например, для синтеза функции f , возвращающей максимум два целых числа, логическая спецификация может выглядеть следующим образом:

$(ж (Икс, y) знак равно Икс \lor ж (Икс, y) знак равно y) \land ж (Икс, y) \geq Икс \land ж (Икс, y) \geq y$

и грамматика может быть:

<  Exp  >   ::=  x |   й |   0 |   1 |   <  Опыт  >  +  <  Опыт  >  |  (  <Cond>   ,   <Exp>    ,  <Exp>   )   ite 
  <  Cond  >   ::=   <  Exp  >  <=  <  Exp  >

где «ite» означает «если-то-иначе». Выражение

ite(x <= y, y, x)

было бы допустимым решением, поскольку оно соответствует грамматике и спецификации.

С 2014 по 2019 год на ежегодном конкурсе синтаксического синтеза (или SyGuS-Comp) сравнивались различные алгоритмы синтеза программ в рамках конкурентного мероприятия. ^[8]В конкурсе использовался стандартизированный формат ввода SyGuS-IF, основанный на SMT-Lib 2 . Например, следующий SyGuS-IF кодирует задачу синтеза максимума двух целых чисел (как представлено выше):

(множественная логика LIA)
 (synth-fun f ((x Int) (y Int)) Int
   ((i Int) (c Int) (b Bool))
   ((i Int (cxy (+ ii) (ite bii)))
    (c Int (0 1))
    (b Bool ((<= ii)))))
 (объявить-var x Int)
 (объявить-var y Int)
 (ограничение (>= (fxy) x))
 (ограничение (>= (fxy) y))
 (ограничение (или (= (fxy) x) (= (fxy) y)))
 (чек-синт)

Совместимый решатель может вернуть следующий результат:

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

Структура Вальдингера Манны и

Правила неклаузального разрешения (объединяющие замены не показаны)
Нет.	Утверждения	Цели	Программа	Источник
51	$E[p]$
52	$F[p]$
53		$G[p]$	с
54		$H[p]$	т
55	$E[{\text{true}}]\lor F[{\text{false}}]$			Решить(51,52)
56		$\lnot F[{\text{true}}]\land G[{\text{false}}]$	с	Решить(52,53)
57		$\lnot F[{\text{false}}]\land G[{\text{true}}]$	с	Решить(53,52)
58		$G[{\text{true}}]\land H[{\text{false}}]$	п ? с : т	Решить(53,54)

Концепция Манны и Вальдингера , опубликованная в 1980 году, ^[9]^[10]начинается с заданной пользователем формулы спецификации первого порядка . Для этой формулы строится доказательство, тем самым также синтезируя функциональную программу из объединяющих подстановок.

Структура представлена в виде таблицы, столбцы которой содержат:

Номер строки («Nr») для справочных целей.
формулы , включая аксиомы и предусловия («Утверждения»). Уже установленные
Формулы, которые еще предстоит доказать, включая постусловия («Цели»), ^{[примечание 1]}
Термины , обозначающие допустимое выходное значение («Программа») ^{[заметка 2]}
Обоснование текущей строки («Происхождение»)

Первоначально в таблицу вводятся базовые знания, предварительные и постусловия. После этого вручную применяются соответствующие правила доказательства. Фреймворк был разработан для повышения удобочитаемости промежуточных формул человеком: в отличие от классического разрешения , он не требует клаузальной нормальной формы , но позволяет рассуждать с формулами произвольной структуры и содержащими любые соединения (« неклаузальное разрешение »). Доказательство завершено, когда ${\it {true}}$ было получено в столбце «Цели» или, что то же самое, ${\it {false}}$ в столбце Утверждения . Программы, полученные с помощью этого подхода, гарантированно удовлетворяют формуле спецификации, начиная с которой; в этом смысле они верны по своей конструкции . ^[11] Только минималистский, но полный по Тьюрингу , ^[12] чисто функциональный язык программирования , состоящий из условных, рекурсивных, арифметических и других операторов. ^{[заметка 3]}поддерживается. Тематические исследования, выполненные в рамках этой структуры, синтезировали алгоритмы для вычисления, например, деления , остатка , ^[13] квадратный корень , ^[14] объединение терминов , ^[15] ответы на к реляционной базе данных запросы ^[16] и несколько алгоритмов сортировки . ^[17]^[18]

Правила доказательства [ править ]

К правилам доказательства относятся:

Неклаузальное разрешение (см. таблицу).

Например, строка 55 получается путем решения формулы утверждения

E

от 51 и

F

из 52, которые имеют общую подформулу

p

. Резольвента образуется в результате дизъюнкции

E

, с

p

заменен на

{\it {true}}

, и

F

, с

p

заменен на

{\it {false}}

. Эта резольвента логически следует из конъюнкции

E

и

F

. В более общем смысле,

E

и

F

нужно иметь только две унифицируемые подформулы

p_{1}

и

p_{2}

, соответственно; их резольвента затем образуется из

E\theta

и

F\theta

как и раньше, где

\theta

является наиболее общим объединителем

p_{1}

и

p_{2}

. Это правило обобщает разрешение статей . ^[19]

Программные члены родительских формул объединяются, как показано в строке 58, для формирования выходных данных резольвенты. В общем случае

\theta

применяется и к последнему. Поскольку подформула

p

появляется в выходных данных, необходимо позаботиться о том, чтобы разрешать только подформулы, соответствующие вычислимым свойствам.

Логические преобразования.

Например,

E\land (F\lor G)

может быть преобразован в

(E\land F)\lor (E\land G)

) как в Утверждениях, так и в Целях, поскольку оба они эквивалентны.

Расщепление конъюнктивных утверждений и дизъюнктивных целей.

Пример показан в строках с 11 по 13 примера игрушки ниже.

Структурная индукция .

Это правило позволяет синтезировать рекурсивные функции . Для данного пред- и постусловия «Дано

x

такой, что

{\textit {pre}}(x)

, находить

f(x)=y

такой, что

{\textit {post}}(x,y)

", а также соответствующее упорядочение , заданное пользователем.

\prec

области

x

, всегда разумно добавить утверждение "

x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))

". ^[20] Решение с помощью этого утверждения может привести к рекурсивному вызову

f

в срок действия Программы.

Пример дан в Manna, Waldinger (1980), стр. 108-111, где синтезируется алгоритм вычисления частного и остатка двух заданных целых чисел с использованием нормального порядка.

(n',d')\prec (n,d)

определяется

0\leq n'<n

(стр. 110).

Мюррей показал, что эти правила полны для логики первого порядка . ^[21] В 1986 году Манна и Уолдингер добавили обобщенные правила электронного разрешения и парамодуляции , чтобы также обеспечить равенство; ^[22] позже эти правила оказались неполными (но тем не менее обоснованными ). ^[23]

Пример [ править ]

Пример синтеза функции максимума
Нет.	Утверждения	Цели	Программа	Источник
1	$A=A$			Аксиома
2	$A\leq A$			Аксиома
3	$A\leq B\lor B\leq A$			Аксиома
10		$x\leq M\land y\leq M\land (x=M\lor y=M)$	М	Спецификация
11		$(x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)$	М	Дистр(10)
12		$x\leq M\land y\leq M\land x=M$	М	Сплит(11)
13		$x\leq M\land y\leq M\land y=M$	М	Сплит(11)
14		$x\leq x\land y\leq x$	Икс	Решить(12,1)
15		$y\leq x$	Икс	Решить(14,2)
16		$\lnot (x\leq y)$	Икс	Решить(15,3)
17		$x\leq y\land y\leq y$	и	Решить(13,1)
18		$x\leq y$	и	Решить(17,2)
19		${\textit {true}}$	х<у ? у : х	Решить(18,16)

В качестве игрушечного примера — функциональная программа для вычисления максимального $M$ из двух чисел $x$ и $y$ можно вывести следующим образом. ^{[ нужна цитата ]}

Начиная с описания требования « Максимум больше или равен любому заданному числу и является одним из заданных чисел », формула первого порядка $\forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)$ получается как его формальный перевод. Эту формулу предстоит доказать. обратной сколемизации Путем ^{[примечание 4]} получается спецификация в строке 10, где прописная и строчная буквы обозначают переменную и константу Скулема соответственно.

После применения правила преобразования распределительного закона в строке 11 целью доказательства является дизъюнкция, и, следовательно, ее можно разделить на два случая, а именно. строки 12 и 13.

Возвращаясь к первому случаю, разрешение строки 12 с аксиомой в строке 1 приводит к созданию экземпляра программной переменной. $M$ в строке 14. Интуитивно понятно, что последнее соединение строки 12 предписывает значение, которое $M$ надо брать в этом случае. Формально правило неклаузального разрешения, показанное в строке 57 выше, применяется к строкам 12 и 1, причем

$p$ является распространенным экземпляром $х=х$ из $А=А$ и $x=M$ , полученный синтаксическим объединением последних формул,
$Ф[$ $п$ $]$ существование $правда \land$ $x=x$ , полученный из созданной строки 1 (дополненной соответствующим образом, чтобы сделать контекст $F[\cdot]$ вокруг $p$ виден), и
$Г[$ $п$ $]$ существование $х \leq х \land у \leq х \land$ $x = x$ , полученный из созданной строки 12,

уступчивость $\lnot ($ $правда \land$ $ложь$ $) \land ($ $х \leq х \land у \leq х \land$ $истинный$ $)$ , что упрощается до $x\leq x\land y\leq x$ .

Аналогичным образом, строка 14 дает строку 15, а затем строку 16 по разрешению. Также второй случай, $x\leq M\land y\leq M\land y=M$ в строке 13 обрабатывается аналогичным образом, в результате чего получается строка 18.

На последнем этапе оба случая (т. е. строки 16 и 18) объединяются с использованием правила разрешения из строки 58; чтобы это правило стало применимым, необходим подготовительный этап 15→16. Интуитивно, строку 18 можно прочитать как «на случай, если $x\leq y$ , выход $y$ действителен (относительно исходной спецификации), а в строке 15 написано «в случае $y\leq x$ , выход $x$ действует; шаг 15→16 установил, что оба случая 16 и 18 дополняют друг друга. ^{[примечание 5]}Поскольку и строка 16, и строка 18 содержат термин программы, условное выражение в столбце программы появляется . Поскольку формула цели ${\textit {true}}$ выведено, доказательство завершено, и столбец программы в " ${\textit {true}}$ " Строка содержит программу.

См. также [ править ]

Примечания [ править ]

^ Различие «Утверждения» / «Цели» предназначено только для удобства; следуя парадигме доказательства от противного , цель $F$ эквивалентно утверждению $\lnot F$ .
^ Когда $F$ и $s$ — формула Цели и срок Программы в строке соответственно, то во всех случаях, когда $F$ держит, $s$ является действительным результатом программы, подлежащей синтезу. Этот инвариант поддерживается всеми правилами доказательства. Формула утверждения обычно не связана с термином Программы.
^ только условный оператор ( ?: С самого начала поддерживается ). Однако можно добавлять произвольные новые операторы и отношения, предоставляя их свойства в качестве аксиом. В приведенном ниже примере игрушки только свойства $=$ и $\leq$ те, которые действительно необходимы для доказательства, аксиоматизированы в строках с 1 по 3.
^ В то время как обычная сколемизация сохраняет выполнимость, обратная сколемизация, то есть замена универсально квантифицированных переменных функциями, сохраняет достоверность.
^ Для этого была необходима Аксиома 3; на самом деле, если $\leq$ не был полным порядком , максимум не мог быть вычислен для несравнимых входных данных $x,y$ .

Ссылки [ править ]

^ Басин, Д.; Девиль, Ю.; Фленер, П.; Хамфельт, А.; Фишер Нильссон, Дж. (2004). «Синтез программ вычислительной логики». У М. Брюйноге и К.-К. Лау (ред.). Разработка программ по вычислительной логике . ЛНКС. Том. 3049. Спрингер. стр. 30–65. CiteSeerX 10.1.1.62.4976 .
^ ( Алур, Сингх и Фисман )
^ Церковь Алонсо (1957 г.). «Применение рекурсивной арифметики к задаче синтеза схем». Итоги Летнего института символической логики . 1 :3–50.
^ Ричард Бючи, Лоуренс Ландвебер (апрель 1969 г.). «Решение последовательных условий с помощью стратегий конечных состояний» . Труды Американского математического общества . 138 : 295–311. дои : 10.2307/1994916 . JSTOR 1994916 .
^ Солар-Лезама, Армандо (2008). Синтез программы путем эскизирования (PDF) (доктор философии). Калифорнийский университет, Беркли.
^ Алур, Раджив; др. и др. (2013). «Синтаксис-ориентированный синтез». Труды по формальным методам автоматизированного проектирования . IEEE. п. 8.
^ Дэвид, Кристина; Кренинг, Дэниел (13 октября 2017 г.). «Программный синтез: проблемы и возможности» . Философские труды Королевского общества A: Математические, физические и технические науки . 375 (2104): 20150403. doi : 10.1098/rsta.2015.0403 . ISSN 1364-503X . ПМЦ 5597726 . ПМИД 28871052 .
^ SyGuS-Comp (Конкурс синтаксического синтеза)
^ Зохар Манна, Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090 . S2CID 14770735 .
^ Зохар Манна и Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническая записка). НИИ Интернешнл. Архивировано (PDF) из оригинала 27 января 2021 г.
^ Правильность правил разрешения см. в Manna, Waldinger (1980), стр. 100.
^ Бойер, Роберт С.; Мур, Дж. Стротер (май 1983 г.). Механическое доказательство полноты по Тьюрингу чистого Lisp (PDF) (технический отчет). Институт компьютерных наук Техасского университета в Остине. 37. Архивировано (PDF) из оригинала 22 сентября 2017 г.
^ Манна, Вальдингер (1980), стр.108-111.
^ Зохар Манна и Ричард Уолдингер (август 1987 г.). «Происхождение парадигмы бинарного поиска». Наука компьютерного программирования . 9 (1): 37–83. дои : 10.1016/0167-6423(87)90025-6 .
^ Даниэле Нарди (1989). «Формальный синтез алгоритма объединения методом дедуктивной таблицы». Журнал логического программирования . 7 : 1–43. дои : 10.1016/0743-1066(89)90008-3 .
^ Даниэле Нарди и Риккардо Розати (1992). «Дедуктивный синтез программ ответа на запросы». В Кунг-Киу Лау и Тиме Клементе (ред.). Международный семинар по синтезу и преобразованию логических программ (LOPSTR) . Семинары по информатике. Спрингер. стр. 15–29. дои : 10.1007/978-1-4471-3560-9_2 .
^ Джонатан Трауготт (1986). «Дедуктивный синтез сортирующих программ». Материалы Международной конференции по автоматизированному дедукции . ЛНКС . Том. 230. Спрингер. стр. 641–660.
^ Джонатан Трауготт (июнь 1989 г.). «Дедуктивный синтез сортирующих программ». Журнал символических вычислений . 7 (6): 533–572. дои : 10.1016/S0747-7171(89)80040-9 .
^ Манна, Вальдингер (1980), стр.99
^ Манна, Вальдингер (1980), стр.104
^ Манна, Вальдингер (1980), стр.103, со ссылкой на: Нил В. Мюррей (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (технический отчет). Сиракузский университет. 2-79.
^ Зохар Манна, Ричард Уолдингер (январь 1986 г.). «Особые отношения в автоматизированном выводе» . Журнал АКМ . 33 : 1–59. дои : 10.1145/4904.4905 . S2CID 15140138 .
^ Зоар Манна, Ричард Уолдингер (1992). «Правила особых отношений неполны». Учеб. КЕЙД 11 . ЛНКС. Том. 607. Спрингер. стр. 492–506.

Алур, Раджив; Сингх, Ришаб; Фисман, Дана; Солар-Лезама, Армандо (20 ноября 2018 г.). «Поисковой программный синтез» . Коммуникации АКМ . 61 (12): 84–93. дои : 10.1145/3208071 . ISSN 0001-0782 .
Зоар Манна, Ричард Уолдингер (1975). «Знание и рассуждение в синтезе программ». Искусственный интеллект . 6 (2): 175–208. дои : 10.1016/0004-3702(75)90008-9 .

[11] Различие «Утверждения» / «Цели» предназначено только для удобства; следуя парадигме доказательства от противного , цель $F$ эквивалентно утверждению $\lnot F$ .

[12] Когда $F$ и $s$ — формула Цели и срок Программы в строке соответственно, то во всех случаях, когда $F$ держит, $s$ является действительным результатом программы, подлежащей синтезу. Этот инвариант поддерживается всеми правилами доказательства. Формула утверждения обычно не связана с термином Программы.

[15] только условный оператор ( ?: С самого начала поддерживается ). Однако можно добавлять произвольные новые операторы и отношения, предоставляя их свойства в качестве аксиом. В приведенном ниже примере игрушки только свойства $=$ и $\leq$ те, которые действительно необходимы для доказательства, аксиоматизированы в строках с 1 по 3.

[27] В то время как обычная сколемизация сохраняет выполнимость, обратная сколемизация, то есть замена универсально квантифицированных переменных функциями, сохраняет достоверность.

[28] Для этого была необходима Аксиома 3; на самом деле, если $\leq$ не был полным порядком , максимум не мог быть вычислен для несравнимых входных данных $x,y$ .

[1] Басин, Д.; Девиль, Ю.; Фленер, П.; Хамфельт, А.; Фишер Нильссон, Дж. (2004). «Синтез программ вычислительной логики». У М. Брюйноге и К.-К. Лау (ред.). Разработка программ по вычислительной логике . ЛНКС. Том. 3049. Спрингер. стр. 30–65. CiteSeerX 10.1.1.62.4976 .

[2] ( Алур, Сингх и Фисман )

[3] Церковь Алонсо (1957 г.). «Применение рекурсивной арифметики к задаче синтеза схем». Итоги Летнего института символической логики . 1 :3–50.

[4] Ричард Бючи, Лоуренс Ландвебер (апрель 1969 г.). «Решение последовательных условий с помощью стратегий конечных состояний» . Труды Американского математического общества . 138 : 295–311. дои : 10.2307/1994916 . JSTOR 1994916 .

[5] Солар-Лезама, Армандо (2008). Синтез программы путем эскизирования (PDF) (доктор философии). Калифорнийский университет, Беркли.

[6] Алур, Раджив; др. и др. (2013). «Синтаксис-ориентированный синтез». Труды по формальным методам автоматизированного проектирования . IEEE. п. 8.

[7] Дэвид, Кристина; Кренинг, Дэниел (13 октября 2017 г.). «Программный синтез: проблемы и возможности» . Философские труды Королевского общества A: Математические, физические и технические науки . 375 (2104): 20150403. doi : 10.1098/rsta.2015.0403 . ISSN 1364-503X . ПМЦ 5597726 . ПМИД 28871052 .

[8] SyGuS-Comp (Конкурс синтаксического синтеза)

[9] Зохар Манна, Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM в языках и системах программирования . 2 : 90–121. дои : 10.1145/357084.357090 . S2CID 14770735 .

[10] Зохар Манна и Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническая записка). НИИ Интернешнл. Архивировано (PDF) из оригинала 27 января 2021 г.

[13] Правильность правил разрешения см. в Manna, Waldinger (1980), стр. 100.

[14] Бойер, Роберт С.; Мур, Дж. Стротер (май 1983 г.). Механическое доказательство полноты по Тьюрингу чистого Lisp (PDF) (технический отчет). Институт компьютерных наук Техасского университета в Остине. 37. Архивировано (PDF) из оригинала 22 сентября 2017 г.

[16] Манна, Вальдингер (1980), стр.108-111.

[17] Зохар Манна и Ричард Уолдингер (август 1987 г.). «Происхождение парадигмы бинарного поиска». Наука компьютерного программирования . 9 (1): 37–83. дои : 10.1016/0167-6423(87)90025-6 .

[18] Даниэле Нарди (1989). «Формальный синтез алгоритма объединения методом дедуктивной таблицы». Журнал логического программирования . 7 : 1–43. дои : 10.1016/0743-1066(89)90008-3 .

[19] Даниэле Нарди и Риккардо Розати (1992). «Дедуктивный синтез программ ответа на запросы». В Кунг-Киу Лау и Тиме Клементе (ред.). Международный семинар по синтезу и преобразованию логических программ (LOPSTR) . Семинары по информатике. Спрингер. стр. 15–29. дои : 10.1007/978-1-4471-3560-9_2 .

[20] Джонатан Трауготт (1986). «Дедуктивный синтез сортирующих программ». Материалы Международной конференции по автоматизированному дедукции . ЛНКС . Том. 230. Спрингер. стр. 641–660.

[21] Джонатан Трауготт (июнь 1989 г.). «Дедуктивный синтез сортирующих программ». Журнал символических вычислений . 7 (6): 533–572. дои : 10.1016/S0747-7171(89)80040-9 .

[22] Манна, Вальдингер (1980), стр.99

[23] Манна, Вальдингер (1980), стр.104

[24] Манна, Вальдингер (1980), стр.103, со ссылкой на: Нил В. Мюррей (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (технический отчет). Сиракузский университет. 2-79.

[25] Зохар Манна, Ричард Уолдингер (январь 1986 г.). «Особые отношения в автоматизированном выводе» . Журнал АКМ . 33 : 1–59. дои : 10.1145/4904.4905 . S2CID 15140138 .

[26] Зоар Манна, Ричард Уолдингер (1992). «Правила особых отношений неполны». Учеб. КЕЙД 11 . ЛНКС. Том. 607. Спрингер. стр. 492–506.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

[примечание 1]

[заметка 2]

[11]

[12]

[заметка 3]

[13]

[14]

[15]

[16]

[17]

[18]

[19]

[20]

[21]

[22]

[23]

[примечание 4]

[примечание 5]