Далее отвечу на основные вопросы, возможные при знакомстве с графит-методом. В сущности, это разные грани вопроса — почему ГРАФИТ? Возможно, по мере расширения аудитории эти вопросы станут часто задаваемыми... :)

Какая верификация нужна для гарантоспособности?

Рассмотрим сущность верификации сложных систем (в частности, программно-аппаратных комплексов).

Как уже говорилось, сегодня активно развивается направление формальной верификации деятельности (программ, описаний трудовых процессов). Это стало возможным благодаря новым результатам в математике и формальной логике (неклассической), полученным в сновном на рубеже столетий. Сжато они были изложены в /п. 4.3.2/ подробному изложению с примерами посвящена работа Ю.Г. Карпова /7/.

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

Этот метод совместим с т.н. доказательным информоделированием (программированием). Поскольку при этом формулируются соглашения (контракты) для программ, которые есть разновидность формальных требований.

А какова позиция по этому вопросу в шампур-визуализации? Можно представить её следующей цитатой из /2, с. 274-275/¹:

Согласно Р. Андерсону, "целью многих исследований в области доказательства правильности программ является... механизация таких доказательств" [10]. Д. Грис указывает, что "доказательство должно опережать построение программы" [11]. Объединив оба требования, получим, что автоматическое доказательство правильности должно опережать построение программы. Нетрудно убедиться, что шампур-метод обеспечивает частичное выполнение этого требования. В самом деле, в начале главы было показано, что любая правильно построенная шампур-схема является строго доказанной теоремой. В алгоритмах ДРАКОН-редактора закодировано исчисление икон, поэтому любая шампур-схема, построенная с его помощью, является истинной, т. е. правильно построенной. Это означает, что ДРАКОН-редактор осуществляет 100%-е автоматическое доказательство правильности шампур-схем, гарантируя принципиальную невозможность ошибок визуального синтаксиса. Поскольку шампур-схема является частью шампур-программы, сказанное равносильно доказательству частичной правильности шампур-программы.

В начале главы мы задали смешной вопрос: если дракон-схемы — это теоремы, кто должен их доказывать? Ответ прост. Их никто не должен доказывать, так как все они раз и навсегда доказаны благодаря тому, что работа ДРАКОН-редактора построена как реализация исчисления икон.

А теперь добавим ложку дегтя в бочку меда. К сожалению, данный метод позволяет доказать правильность шампур-схемы и только. Это составляет лишь малую часть от общего объема работы, которую нужно выполнить, чтобы доказать правильность программы на все 100%. Правда, есть небольшое утешение: частичное доказательство правильности программы с помощью ДРАКОН-редактора осуществляется без какого-либо участия человека и достигается совершенно бесплатно, так как дополнительные затраты труда, времени и ресурсов не требуются. А дареному коню в зубы не смотрят.

Итак, шампур-метод как математически формальная основа информоделирования обеспечивает доказательное построение лишь структуры маршрутов — т.е. порядка следования вершин графа алгопроцесса (программы). Как же выполняется оставшаяся «большая часть» работы по верификации?

В условиях, когда сочинитель может представлять себе состояние исполнителя, следование по маршрутам сочиняемого процесса вызывает у него образ меняющегося состояния. Это служит существенной поддержкой для «мозговой проверки» правильности сочинения. Такое возможно, в частности, при программировании в кодах информашины с ограниченной ОП и относительно простой программистской архитектурой и системой команд. Проверка может осуществляться методом «прокрутки», как описано в /Звенигородский, 1985, с. 117...120/, причём по машинным командам. Шампур-силуэт естественно представляет программу как код с явными БП, а визуальный оператор м.б. представлен одной вершиной.

Многие же современные информашины архитектурно сложны, их команды оперируют одновременно с большим числом ПДЭ и реализуют сложную структуру действий, часто взаимозависимых. Достаточно вспомнить команды защищенного режима МП семейства Интел 80NNN. В этих условиях сочинителю сложно, а чаще невозможно заниматься «прокруткой», да ещё покомандной.

Заметим, что хакерам программ иногда приходится действовать именно так — но для достаточно коротких фрагментов программы, допускающих скрупулёзное исследование при разумных затратах времени и сил. Кроме того, их цели обычно не подразумевают гарантоспособности результата. :) Скорее это рассматривается как игра с кодом под отладчиком — кстати, с недавних пор существует выражение «самая увлекательная пошаговая «стратегия» - дебаггер» :)) (С. Губанов)².

Возникает необходимость в абстрагировании, выходе на более высокие уровни. В первую очередь — операторов прогязыка ВУ, используемого при сочинении. Одновременно нужно рассуждать в терминах величин программы и их абстрактных типов. И заменять образ состояния исполнителя на систему соотношений между величинами, выполняемость которой на каждом шаге означает правильность исполнения этого шага. Здесь перестают работать сразу два принципа «исходной» дракон-методологии:

От явных БП уходят именно в целях доказательного информоделирования — т.к. для представления результатов логического вывода условий нелинейной маршрутной алгоструктуры и требований к величинам алгопроцесса необходимы и достаточны только комбинации элементарных следований, ветвлений, циклов.

Однако это не значит, что не будет работать шампур-метод. Просто нужно найти структуры, адекватно отображаемые на такие языки, а если нужно - модифицировать метод так, чтобы отображение стало возможным. В частности, необходимы и достаточны только атомарные шампур-структуры — т.е. полученные лишь с помощью операции ввода атома.

Главной нелинейной структурой доказательного информоделирования становится т.н. цикл Дейкстры (ЦД), обсуждавшийся в /3, п/п 2.2.3.1/. Посредством ЦД можно представить и шампур-силуэт; это означает, что возможен вполне тривиальный перевод существующих визуалов в форму, верифицируемую методом проверки моделей. Однако лучше с самого начала доказательно визуализировать деятельность.

Важно понимать, что если не проделаны «все 100%» работы по верификации — информодель (в частности, запись программы) не может считаться гарантоспособной в современных условиях.

Кстати, о «бесплатности» полной верификации, если понимать её в буквальном смысле. Уже существуют среды автоматизированной верификации, среди которых есть свободно распространяемые. Их перечень можно найти в работе Ю.Г. Карпова /7/.

Если же мы хотим приложить техноязык к визуализации структуры произвольной деятельности — то возникает необходимость в теории деятельности. Именно на её основе м.б. определена лексика (простые и составные атомы), адекватная содержанию мыслимых процессов и систем процессов.

Произвольное построение лексических единиц и их комбинирование может лишь ухудшать понимаемость описаний.

Как же доказательно строить информодели? Это, безусловно, и наука, и инженерное творчество. Простого пути здесь нет; но могут помочь хорошие книги. Пока их ещё немного — можно порекомендовать работы Н. Вирта (прежде всего «Алгоритмы и структуры данных...»), «Дисциплину программирования» Д. Гриса и книгу Карпова /7/. Правда, нельзя сказать, что они вполне удовлетворяют критериям когнитивной эргономики — но может быть, более совершенную в этом смысле книгу со временем напишете Вы?.. :)

Интеллектуальный терроризм, преступная халатность или ?..

Определённого уточнения заслуживает и понятие «интеллектуального терроризма», введённое Паронджановым. Напомним его авторское определение из /2, с. 16/:

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

Полагая, что мы находимся в правовом государстве, сопоставим с законодательным определением терроризма³:

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

наказываются лишением свободы на срок от восьми до пятнадцати лет.

а) совершенные группой лиц по предварительному сговору или организованной группой;

б) повлекшие по неосторожности смерть человека;

в) повлекшие причинение значительного имущественного ущерба либо наступление иных тяжких последствий, -

наказываются лишением свободы на срок от десяти до двадцати лет с ограничением свободы на срок от одного года до двух лет.

3. Деяния, предусмотренные частями первой или второй настоящей статьи, если они:

а) сопряжены с посягательством на объекты использования атомной энергии либо с использованием ядерных материалов, радиоактивных веществ или источников радиоактивного излучения либо ядовитых, отравляющих, токсичных, опасных химических или биологических веществ;

б) повлекли умышленное причинение смерти человеку, -

наказываются лишением свободы на срок от пятнадцати до двадцати лет с ограничением свободы на срок от одного года до двух лет или пожизненным лишением свободы.

Примечание. Лицо, участвовавшее в подготовке террористического акта, освобождается от уголовной ответственности, если оно своевременным предупреждением органов власти или иным способом способствовало предотвращению осуществления террористического акта и если в действиях этого лица не содержится иного состава преступления.

Расхождения очевидны. В основе лежит то, что терроризм — активное нанесение ущерба во имя тех или иных целей (выгод, амбиций, комплексов и пр.). Здесь же ущерб не выступает средством достижения целей — он вытекает из непринятия мер по предотвращению/предолению ущерба от средств/способов достижения внешне допустимого качества, но обнаруживающих на практике опасные свойства.

Поэтому формально-юридически в большинстве ситуаций, неформально обозначенных Паронджановым как «интеллектуальный терроризм», следует говорить о преступной халатности и/или злоупотреблении должностными полномочиями, и/или служебной некомпетентности (в данном случае - в сфере когнитивной эргономики), и/или нарушении безопасности труда.

Социально-экономически же основной корень возникновения данной ситуации — избыточная эксплуатация наёмного работника. Иной раз то же можно сказать и об отношении собственника к потребителям (эксплуатантам).

Некомпетентность собственника средств производства именно как собственника выступает, по-видимому, решающим условием. Потому что главной компетенцией здесь выступает отнюдь не управление финансовыми и товарными потоками (для этого обычно есть управленцы — опять же наёмные) — но способность отвечать за риски не только для себя, но и для других, не только сиюминутные, но и долгосрочные.

Почему говорится «отвечать», а не, скажем «выявлять»? Потому что собственник дела не обязан быть специалистом в самых разных предметных областях, где риски могут возникнуть. Но именно ответственность побуждает его систематически, перманентно организовать и вести выявление и анализ рисков силами специалистов в соответствующих «предметках» - конечно, учёных и аналитиков прежде всего. По сути, это обеспечение эффективности в широком смысле (в современном определении; см. ст. Показатель эффективности в /3, п. 1.1.2/).

Замечу, что такое переопределение не снижает остроты проблемы и в морально-этическом плане, и в социально-политическом. Достаточно вспомнить, как осенью 2010 года взбудоражили общество «инициативы» ряда крупных собственников средств производства на территории России об увеличении рабочего дня и/или недели, возможном сокращении социальных гарантий — во имя формально-сиюминутно трактуемой «производительности труда».

Существенно обострилась ситуация с широким распространением в последние десятилетия т.н. инвестиционного механизма ценностного обеспечения деятельности (привлечения прежде всего денежных средств, но также и иных ценностей). Возможная природа этого вскрыта в работе /Девятов, Мартиросьян, 2002/ (см. также в /3, п. 5.2.2/).

Так что же, говорить о «террористической угрозе» в связи с умственным трудом вообще и в частности — в связи с разработкой программных и иных искусственных систем — не приходится? Это не совсем так. Только нужно взглянуть на ситуацию несколько под иным углом зрения.

Обратимся для начала всё к той же работе /6/. В п. 1.1 Карпов приводит примеры последствий ошибок в программных системах. В результате, как видно из сказанного, некоторые изделия, работая под управлением этих программ, превращаются в эквиваленты орудий террора. Но напомним сказанное выше — в этих случаях никто их такими не создавал специально или не проявлял нежелание освободить от ошибок, буде возможно их обнаружить.

Основное же содержание цитируемой работы — как раз методы верификации, дающие такую возможность. Методы эти известны около 20 лет, принципиальные для широкого практического применения результаты получены более 10 лет назад, и с этого времени ответственными разработчиками они применяются и развиваются.

Замечу, что методы доказательной формализации и формальной верификации, конечно, для сегодняшнего уровня математической культуры в ИТ-отрасли нетривиальны. Поэтому их применение потребует определённых усилий. Оправданно будет начинать с задач «кризисных» в определении известного отечественного ИТ-специалиста Г.Р. Громова.

Ключевое же условие верифицируемой разработки - соблюдение определённой дисциплины во всех трёх «китах» МФЗ — свойствах языка, технологии и реализации. В частности, следует пользоваться гарантоспособными языками и средами программирования (и спецификации задач). И вот на этом фоне заявления такого рода:

Вы никогда не построите генератор в Яву. Ява хоть и значительно синтаксически проще современного С#, модульный подход ООП требует архитектуры, а архитектура требует творчества. Нету даже нормальных генераторов из C# в Яву и обратно, хотя синтаксически эти языки очень схожи.

- звучат и правда как пропаганда если не терроризма, то экстремизма в профессиональной деятельности. Потому что «творчество» здесь понимается как свобода от формального синтаксиса и математически точного представления об архитектуре системы — соблюдение этих условий и даёт возможность формально верифицировать код (и/или его спецификацию).

Может возникнуть вопрос: а почему такие заявления можно отнести к экстремизму? Возьмём его официальное определение:⁴

В России юридическое определение того, какие действия считаются экстремистскими, содержится в статье 1 Федерального Закона № 114-ФЗ «О противодействии экстремистской деятельности».[7]⁵

В соответствии с поправками от 29 апреля 2008 г. к экстремистской деятельности (экстремизму) относятся:

Здесь существенно определение "исключительности, превосходства либо неполноценности человека по признаку его ... языковой принадлежности." как экстремизма. Конечно, гражданин может возразить - "Так это разве не о естественных языках?" - но формулировка закона оснований к такому сужению не даёт... Кроме того - выше мы уже говорили о последствиях такого поверхностного (мягко говоря) отношения к качеству искусственных языков и записей на них как к изделиям.

Автор отнюдь не считает эти оценки обращением к «компетентным органам» с целью немедленно «разобраться как следует и наказать кого попало» ;). Тем более что методы формальной верификации, практической реализации которых, как уже сказано, порядка 10 лет, сегодня широкие массы аналитиков и программистов ещё могут не знать — и, возможно, именно этим подчас объясняется позиция, обозначаемая подобными заявлениями.

Но ещё раз посмотрим на примеры у Карпова и Петрова — опасность в результате «бездоказательного» построения и «неформальной» верификации могут заключать самые широко используемые изделия. И если и после ознакомления с методами и средствами доказательного программирования (и моделирования задач вообще) кто-либо будет отрицать их необходимость по крайней мере для «кризисных» задач и/или защищать методы и средства (в частности, языки и парадигмы программирования), не допускающие доказательности построения решений, их формальной верифицируемости — это уже позиция преступная :|. И её носители должны отвечать — не только перед законом, но прежде всего перед моралью. Тем более, что мы видим по сути не новое явление из разряда «каждый суслик - агроном», когда люди вне науки (либо недостаточно подготовленные в данной научной отрасли) пытаются давать оценки правильности и/или полезности научных результатов.

Возможен вопрос: полноте, а вообще реален такой уровень ответственности разработчика даже в «кризисной» отрасли? Безусловно — примером тому В.Г. Грабин, разработчик знаменитй пушки-«дивизионки» ЗИС-3 и ряда других орудий, с которыми мы разгромили фашизм в Великой Отечественной войне. Об атмосфере в его КБ даёт представление следующий случай⁶.

Пример: проектирование, эффективное в широком смысле. Для КБ Грабина с самого начала было характерно тесное сотрудничество с технологами производства. Один из конструкторов, проектируя свой агрегат пушки, обсуждал промежуточные результаты с технологом. Тот заметил ему: «вот эту деталь ты сделал сложного профиля; а поскольку она протяжённая, придётся для её обработки применить подвижной люнет⁷ — а ведь это народные деньги!». Конструктор деталь упростил.

К сожалению, в условиях массово распространённого «служебного несоответствия» сбственников и высших руководителей мы имеем примеры обратные — небрежения ресурсами и жизнями людей — и не только участников производства, но и потребителей. Ещё один пример тому приводит среди прочих Ю.П. Петров в одной из своих работ⁸.

Пример: негарантоспособная разработка. Компания «Эйрбас» столкнулась с аномальным поведением систем управления двигателями на своих аэробусах А-310 и А-320. При посадке в ответ на команду реверса тяги СУД могли... разгонять двигатели на прямой тяге, что, естественно, вело к лётным происшествиям и даже к серьёзным катастрофам, в т.ч. с человеческими жертвами. Руководствуясь данными «чёрных ящиков» Петров с сотрудниками, следуя своему открытию о несохранении при некоторых условиях корректности результатов математических преобразований в случаях вариаций числовых параметров, обнаружили признаки нарушения корректности модели управления. Однако производитель не отреагировал на предложения о совершенствовании системы и продолжал поддерживать версии об ошибках пилотов.

Здесь мы как раз видим отсутствие ответственности за риски, продуцируемые изделием.

К чему всё это говорилось здесь, в связи с методами формализации? Дело в том, что любой метод нужно внедрять в практику — и данный ресурс в конечном счёте служит поддержке такого внедрения. А возможность внедрить в конкретной организации зависит в немалой степени от компетентности собственников (в определённом выше смысле) — ну и руководителей (позиция которых зачастую не менее активна). Там, где ответственность за все возможные эффекты дела — и позитивные, и негативные, и «для себя», и «для других» - ослаблена или тем более не просматривается вообще — там вряд ли можно говорить о внедрении техноязыка, а тем более чего-то более развитого.

Визуализация грамотно проектирует мозг сама по себе?

В /2, Гл. 20/ приложение визуализации обосновано теорией интенсификации интеллекта. Выдвинутая создателем техноязыка, она базируется на результатах наук о человеке и живой природе, полученных на конец прошлого века. С тех пор, однако, получены некоторые новые результаты и выдвинуты новые объяснения работы ума. Покажем, что это, не отрицая визуализации, ставит её в более широкий контекст — и предъявляет к ней определённые требования, необходимые для достижения целей стратегической интеллектуальной инициативы.

Удобно взять конкретную современную теорию мышления и с её участием продемонстрировать этот самый контекст. Возьмём т.н. теорию двух типов ума; её автор — отечественный физик и ИТ-специалист Ф.В. Ткачёв. Кстати, такое сочетание весьма не случайно — если посмотреть историю науки и техники последних десятилетий, то можно видеть, что именно в физике зародилось и широко развито утилитарное ИТ-производство (и, как следствие, та самая автоформализация знаний, о которой мы тут в основном и толкуем).

Чтобы не «выжимать самостоятельно суть, дабы объяснить предмет человеку с улицы», как делают некоторые «популяризаторы», приведём краткую характеристику теории непосредственно из уст её автора — а уж затем будем наворачивать на неё собственные соображения. ;)

Итак, вот сообщение, помещённое автором теории на одной веб-конференции (здесь он выступает под псевдонимом Info21):

Первый умотип -- врожденное свойство. Даден всем в разной степени (включая шимпанзе, ворон, попугаев, слонов, ... даже голубей), но в какой-то степени может развиваться, даже довольно заметно (опять же, не у всех). В этих смыслах подобен таким качествам, как выносливость и т.п.

Второй умотип -- это достаточно редкая аномалия, развивающаяся после рождения на основе некоторых врожденных свойств (склонность к рефлексии, к исследовательскому поведению -- на которую тут резко нападали в связи со старым Шнобелем свежего нобелеата Гейна).

Аномалия -- т.к. требует ослабленных нормальных (приматических) мотиваций, а такое ослабление автоматом приводит к сокращению потомства

Но поскольку эта аномалия полезна приматической стае как целому, то в конкуренции социумов кое-как вырабатываются способы иметь загородки, внутри которых есть условия для развития и функционирования второго умотипа (университет со стипендиями для студентов, профессорскими tenure и т.п.).

Сюда относятся улучшения ума из указанного источника⁹ и практически всех подобных книг.

Другое дело, что если такое обучение падает на почву предрасположенности к рефлексии, то оно поспособствует и развитию второго умотипа, хотя само по себе к этому не приведет.

Второй (абстрагирующий/концептуализирующий/рефлексирующий) умотип для своего развития требует:

Хорошая аналогия -- выездка иноходцев: если "загнать" жеребенка-иноходца, то он срывается в галоп, и потом уже вместо иноходи будет бежать банальной рысью.

На самом деле жесткого разграничения индивидов по умотипам, как я понимаю, нет -- как и в случае с психологическими типами А и Б.

Но у обеих этих шкал есть вполне выраженные концы.

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

Можно сказать еще, что второй умотип -- это надстройка над некоторой хорошей базой из первого (иначе чел нарефлексирует такого...).

Но! высокая комбинаторная одаренность (быстрая память и т.п.) может препятствовать развитию критической рефлексии, т.к. индивид со своей быстрой соображаловкой проходит сквозь всё обучение с детсада и по (включая) постдоковский уровень как нож сквозь масло -- ему просто нет нужды развивать что-то там еще.

Такие примеры вокруг науки я имел возможность близко наблюдать не один и не два.

Вот в этом пункте ключевую роль играют мотивации, темперамент и предрасположенности.

Отсюда следует вывод и о роли формы представления (и её качества) в формализации знаний. Вывод такой - эргономика представления сама по себе, а характер мышления сам по себе (как и его эффективность "в широком смысле"). Это просто разные измерения раскрытия объёма понятия умственного труда. Думаю, для вчитавшегося в цитированное сообщение и топик вокруг него это не будет неожиданным.

В частности, в эргономичной записи стоит представлять содержание "в ограничениях на [поверхностное ]комбинирование", чтобы высвобожденную (теоретически) часть усилий ума направить на "абстрагирование/концептуализацию/рефлексию". Которая, между прочим, необходима и для хорошей схематизации знаний. Нет ограничений - и вся высвобожденная часть направляется на усиленные/ускоренные "прыжки за бананами" - только визуализированные...

И ограничения должны закладываться уже в языки представления знаний - по крайней мере, в информатические (возможно, в "гарантоспособные" диалекты/расширения). И в рассуждениях о формализации неплохо их придерживаться...

Теперь попробую более общую вещь сформулировать. Теория интенсификации рассматривает интеллект как "чёрный ящик", который из неких соображений, установленных методами "нормальной науки", можно "грамотно проектировать" подбором формы внешних воздействий данными. Главное соображение - гипотеза Уорфа. Её суть — язык формирует мышление.

А теория, адекватная вызову "отчуждения над-синтаксического" (сейчас ставится и такая задача), должна, полагаю, иметь в основе "белый ящик" - т.е. модель механизмов мышления. И теория умотипов - попытка такую модель дать.

И можно видеть два "но" к существующему (и оформленному фактически теорией интенсификации в опубликованной версии) положению дел.

Во-первых, сегодня говорится о справедливости также утверждения, обратного уорфову - т.е. что и мышление формирует язык. В некотором смысле проект Информатика-21, развиваемый автором теории умотипов - утверждение необходимости нестихийности этого формирования в информатике. И любое средство передачи данных нужно делать не только сокращающим затраты умственного труда — но и нацеливающим ум на «работу над собой», на подъём к абстрагированию, критическому рассмотрению продуктов своего (и чьего-либо) труда.

Во-вторых, есть ещё гипотеза "двойного кодирования" (Р. Солсо) - что мозг пользуется и вербальным, и невербальным представлением. Поэтому владеть и графическим, и текстовым представлением одного и того же — в некотором смысле то же самое, что уметь стрелять «по-македонски» (с двух рук).

В то же время шампур-метод как работа только с силуэтно-разрешёнными явными БП - это, безусловно, ограничение комбинирования структур управления над "чисто приматическим" в виде произвольного явного БП (в текстовой записи - goto). Вопрос только в том, как его излагать.

Дальнейшее же ограничение исходит из осознания того, что явный БП нужен только при работе "в кодах" исполнителя явно-адресной архитектуры (скажем, фон-неймановской, машины Тьюринга с нумерованными ячейками лент[ы]). А в высокоуровневом описании алгоритма нужно, условно говоря, обходиться только БП, "спрятанными" в соединители ветвлений и циклов. Отсюда и замена "паттерна универсальной программы" с силуэта на цикл Дейкстры ("примитивно скомбинированный" переводом из шампур-силуэта - либо "абстрактно концептуализирующий" напрямую решение задачи - в частности, через автоматное представление).

Продолжение ограничения связано с подстановкой и объединениями.

Итак, само по себе ничего не бывает — и эргономичную форму можно использовать по-разному. И получить «по-разному спроектированный» мозг...

В целом из сказанного вытекает такая стратегия — при обучении формализации обязательно пользоваться наиболее строгим языком. Именно так обучаемый может выработать навык построения гарантоспособных моделей.

1 Ссылки в тексте см. по списку литературы в источнике.

2 Источник — это веб-сообщение.

3 См. также: Википедия. Категория «Терроризм»; юридический комментарий.

6 Грабин В.Г. Оружие победы. - М.: Республика, 2000. - С. 419-420.

7 Люнет — род технологического приспособления, употребляемого при станочной обработке длинномерных деталей (как правило, заказного под конкретную форму детали); подвижной отличается существенной конструктивной сложностью.

9 Имеется в виду материал /2, Гл.20/.