Cтраница 1
Абстрактная интерпретация помогает определить характеристики работы программы, что позволяет модифицировать правила для ее вычисления без изменения ее семантики. [1]
Корни теории абстрактной интерпретации находятся в теории доменов, и поэтому полное рассмотрение не только выходит за рамки этой книги, но само по себе требует отдельной книги, В предыдущих разделах мы рассматривали главным образом два семантических направления: стандартную семантику, определенную на стандартном домене D2 и абстрактную семантику с абстрактной областью /) Таким образом, мы должны рассматривать две семантические фуикцуш, отображающие синтаксис данных выражений в величины в стандартных и абстрактных доменах соответственно, а также подходящую функцию абстракции absp, для которой выполняется условие надежности. Следующее описание полностью основано на подходе, описанном в [17], и применяется к функциональным языкам вообще с функциями более высоких порядков, хотя в указываемой работе не рассматриваются неплоские домены. [2]
Доказательство надежности абстрактных интерпретаций относится к области денотационной семантики. [3]
Другие применения абстрактной интерпретации состоят в изменении на месте структур данных, анализе сложности и анализе высказываний. [4]
Впервые мысль о применимости абстрактной интерпретации для анализа строгости была высказана в [69], который использовал эту методику также для исследования проблемы установления условной конечности времени вычисления выражения. Основной задачей здесь является повышение эффективности ленивой реализации функционального языка путем поиска возможности доступа к аргументам по значению, а не по необходимости без изменения условий окончания работы программы. Как мы видели в предыдущих главах, это устраняет необходимость в создании задержек для аргументов в SECD-машине и в то же время уменьшает количество структур данных, создаваемых во время прогона программы и обрабатываемых в дальнейшем сборщиком мусора. Более того, если при параллельной редукции графов известна строгость каждой определенной пользователем функций, то это позволяет производить вычисление строгих аргументов параллельно с вычислением функции, увеличивая тем самым степень параллелизма. [5]
Геометрическое пространство есть результат абстрактной интерпретации оптического пространства, - интерпретации, которая лишает индивидуальных свойств, обобщает ц делает более доступными для ума отношения, заключающиеся в этом оптическом пространстве. [6]
Объясните, что понимается под надежностью абстрактной интерпретации, и дайте формальное описание в терминах соответствующих семантических доменов. Докажите, что в упражнении 20.1 пример с порядком величины является надежным. [7]
Второй рассматриваемый нами подход к повышению эффективности выполнения функциональных программ использует абстрактную интерпретацию для управления путем выполнения программы без модификации ее определения. Механизм такого управления формализуется аннотированием программы, специфицирующим ее операционную семантику более точно, чем это может быть сделано при определении только семантики для языка в целом. Например, мы уже сталкивались в нескольких случаях с семантикой энергичного и ленивого вычислений в функциональных языках, в которых параметры всегда берутся по значению и по необходимости соответственно. Однако нет причины, почему бы не сделать некоторые применения функции энергичными и их аргументы будут браться по значению, а другие - ленивыми и их аргументы будут браться по необходимости. Требуется только однобитовая аннотация для каждого параметра определения функции, указывающая, какая семантика должна быть для каждого компилируемого применения функции. Правда, практическая задача заключается прежде всего в осуществлении правильного выбора. [8]
С одной стороны, мы исследуем преобразование программ, при котором может быть модифицирована вся структура функциональной программы, а с другой стороны, можно управлять выполнением программы, используя аннотации, порождаемые абстрактной интерпретацией. Однако для имеющих точную математическую семантику функциональных языков и преобразование, и абстрактная интерпретация являются методами, способными обеспечить требуемый семантически корректный тип оптимизации. Что касается терминологии, то существует мнение, что преобразование означает любую семантически корректную оптимизацию, поэтому абстрактную интерпретацию можно было бы рассматривать только как часть инструментального набора преобразований. В то же время любой формальный статический анализ программ, включая преобразование, является абстрактной интерпретацией. Существует множество явных ограничений по производительности в неоптимизированых реализациях функциональных языков, разумеется, для последовательных архитектур фон-неймановского типа. Например, применение многих функций при вычислении обладает линейной зависимостью от размера аргумента ( формальные определения в гл. Мы уже увидели примеры этого в авторекурсии, которую, как показано в гл. Аналогично можно было бы ожидать, что при выполнении применения функции Фибоначчи используется число вызовов функции, зависящее экспоненциально от аргумента, тогда как два последовательно накапливающих счетчика дают тот же результат за линейное время и постоянное пространство в императивном цикле. Вопрос, будет ли это несущественно в специализированной, предположительно параллельной архитектуре, в значительной степени неуместен. С одной стороны, фон-неймановские машины останутся и в ближайшем, и в далеком будущем, а в любом случае параллельные машины - это набор последовательных процессоров, каждый из которых лучше всего используется при выполнении нетривиальных преобразований. [9]
Говоря точнее, необходимо с каждым элементом из абстрактного домена Z связать подмножество стандартной области определения Z, которое этот элемент представляет. Абстрактная интерпретация будет корректной и, как говорится, надежной, если реальный результат применения функции находится в наборе, выраженном результатом соответствующего применения абстрактной функции. [10]
Подобный анализ во время компиляции называют анализом строгости. Мы будем использовать его для иллюстрации более общего метода абстрактной интерпретации, который, говоря кратко; выводит определенные свойства выполнения программ, работая с абстрактным доменом, гораздо более простым, нежели ( стандартный) семантический домен анализируемых выражений. Другое применение абстрактной интерпретации возникает в системах вывода типов, образующих основу алгоритмов проверки типов, несмотря на то что термин абстрактная интерпретация еще не был введен в то время, когда были написаны первые программы проверки типов. Проверка типов во время компиляции, разумеется, имеет отношение к оптимизации, но уже рассмотрена в гл. [11]
Существует, однако, большое число иных возможностей ее использования при оптимизации функциональных программ путем семантически корректной аннотации. Мы уже встречались с одним примером, который может рассматриваться как абстрактная интерпретация в системе вывода типов, обсужденной в гл. Проверка типов является полностью статичным анализом, проводящимся на этапе компиляции и может быть сформулирована в терминах отображений между различными семантическими доменами, что является сутью абстрактной интерпретации. После этого могут быть установлены надежность и полнота. [12]
С одной стороны, мы исследуем преобразование программ, при котором может быть модифицирована вся структура функциональной программы, а с другой стороны, можно управлять выполнением программы, используя аннотации, порождаемые абстрактной интерпретацией. Однако для имеющих точную математическую семантику функциональных языков и преобразование, и абстрактная интерпретация являются методами, способными обеспечить требуемый семантически корректный тип оптимизации. Что касается терминологии, то существует мнение, что преобразование означает любую семантически корректную оптимизацию, поэтому абстрактную интерпретацию можно было бы рассматривать только как часть инструментального набора преобразований. В то же время любой формальный статический анализ программ, включая преобразование, является абстрактной интерпретацией. Существует множество явных ограничений по производительности в неоптимизированых реализациях функциональных языков, разумеется, для последовательных архитектур фон-неймановского типа. Например, применение многих функций при вычислении обладает линейной зависимостью от размера аргумента ( формальные определения в гл. Мы уже увидели примеры этого в авторекурсии, которую, как показано в гл. Аналогично можно было бы ожидать, что при выполнении применения функции Фибоначчи используется число вызовов функции, зависящее экспоненциально от аргумента, тогда как два последовательно накапливающих счетчика дают тот же результат за линейное время и постоянное пространство в императивном цикле. Вопрос, будет ли это несущественно в специализированной, предположительно параллельной архитектуре, в значительной степени неуместен. С одной стороны, фон-неймановские машины останутся и в ближайшем, и в далеком будущем, а в любом случае параллельные машины - это набор последовательных процессоров, каждый из которых лучше всего используется при выполнении нетривиальных преобразований. [13]
Использование вместо функции эквивалентной ей запоминающей функции может рассматриваться как результат преобразования программы. Подобно этому, любое предсказание упо-требимости образов значений аргументов в целях управления таблицей можно рассматривать как вид абстрактной интерпретации, и, разумеется, всякое формальное доказательство семантической корректности реализации запоминания для заданной стратегии замещения элементов таблицы потребует методов подобного вида. [14]
Подобный анализ во время компиляции называют анализом строгости. Мы будем использовать его для иллюстрации более общего метода абстрактной интерпретации, который, говоря кратко; выводит определенные свойства выполнения программ, работая с абстрактным доменом, гораздо более простым, нежели ( стандартный) семантический домен анализируемых выражений. Другое применение абстрактной интерпретации возникает в системах вывода типов, образующих основу алгоритмов проверки типов, несмотря на то что термин абстрактная интерпретация еще не был введен в то время, когда были написаны первые программы проверки типов. Проверка типов во время компиляции, разумеется, имеет отношение к оптимизации, но уже рассмотрена в гл. [15]