Подпрограммы

• Процедуры — наиболее общие подпрограммы. Могут содержать выходные параметры и побочные эффекты. Возвращаемое значение необязательно.
• Функции — ограниченные подпрограммы без внешних побочных эффектов с входными неизменяемыми параметрами и возвращаемым значением. Внутри себя могут содержать локальные побочные эффекты
  • Константные функции — тривиально вычислимые на этапе трансляции для константых параметров. Не содержат циклов и рекурсивных вызовов.

Возвращаемое значение у подпрограммы связано со специальной переменной, объявляемой в сигнатуре после параметров. Единственным способом задания возвращемого значения является присвоение значения в эту переменную. Она не может остаться неначализированной.

section example0 {
 const (
  infoSize = 4;
  
  //константные функции объявляются в разделе констант
  func optimalAllocSize(main, x0 int) (x1 int) {
    var (total, fixed int)
    
    fixed := main + infoSize;
    total := x0 + fixed;
    if (total <= 16)
      total := 16
    else
      total := -(-total) / 32 * 32
    end;
    x1 := total - fixed
  }
  
  //такие функции можно использовать для получения констант
  dataSize = optimalAllocSize(33, 22)
  
 )
 
 //эта функция содержит цикл и не может возвращать константы 
 func min(a []int) (val int) {
  var (i int)

  val := a[0];
  for (i = 1; i < len(a); i += 1)
    if (val > a[i])
      val := a[i]
    end
  end
 }

 // процедура с изменяемыми параметрами 
 proc swap(<>a, <>b int) {
  var (t int)
  t := a;
  a := b;
  b := t
 }
 
 proc test(a, b int) {
  var (c, d int)
  // константные функции можно использовать и для переменных
  c := optimalAllocSize(a, b);
  d := 1;
  swap(<>c, <>d)
 }
 
}.

Разновидности параметров

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

• По значению — без отметок.
• Ссылочный параметр. Обозначается знаками «<>». Используется для чтения и записи в произвольном порядке.
• Выходной параметр. Требует предшествующего знака «>». Перед чтением в самой процедуре требует предварительного присваивания. Если его не было, то после вызова процедуры значение параметра должно считаться неначализированным. Возможность отсутствия присваивания должна быть указана в объявлении, иначе это считается ошибкой.
• Ссылочный параметр только для чтения. Предназначен только для параметров структурного типа (массивов и записей) для избежания избыточного копирования и для обобщённого кода. Предваряется знаком «<», но не обязателен для открытых массивов, так как они в общенм случае и так не могут передаваться по значению.
• Закрываемый параметр. Обозначается буквой «Х»(необязательно «X>»). После вызова процедуры переменная-фактический параметр считается неначализированной.

section example1 {
 type ( file { i int } )
  
 proc open(>f file) {
  f.i := 0
 }
  
 proc read(<>f) (val int) {
  val := f.i;
  f.i += 1
 }
  
 proc close(Х f file) {
  // X f // подразумевается неопределённость в f
 }
  
 proc test {
  var ( f file; i int )
  //i := read(<>f);// ошибка трансляции
  open(>f);
  i := read(<>f);
  close(X f);
  // i := read(<>f); // ошибка трансляции
  open(>f)
 }
}.

Утверждения в подпрограммном типе. Пред- и пост- условия

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

section range {

 type ( +t { +@min, +@max int } )

 proc +init(>r t, mn, mx int)
 [ // предусловие
  ! mn <= mx
 post: // постусловие
  ! t.min = mn
  ! t.max = mx
 ]
 {
  t.min := mn;
  t.max := mx
 }

}.

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

Утверждения, которые верны и для пред-, и для пост- условий, можно не дублировать, а записать один раз после «inv:», находящегося между их секциями.

• Пред- и пост- условия состоят из утверждений, разрешений и ветвлений
• В каждом утверждении обязан присутствовать хотя бы один из параметров
• Из подпрограмм в выражениях утверждений могут использоваться только константные функции. Механизм предназначен для сравнительно легковесных проверок
• Выходные параметры «>» не могут присутствовать в предусловиях
• Закрываемые параметры «X» не могут присутствовать в постусловиях
• Нарушение утверждений в вызовах подпрограмм считается ошибочным состоянием, кроме случая явного учёта правильности
• Применение в утверждениях непрозрачных предикатов тоже считается ошибочным состоянием, хотя в общем случае и сложно диагностируемым

Проверка параметров

Предусловия можно использовать для проверки входных параметров с помощью механизма явного взятия правильности

section example2 {

 import ( range, log )
 
 var (a, b int)

 proc +test {
  var (r range:t; ok bool)

  /* мягко проверяются только утверждения, 
    куда входят параметры, помеченные «?» */
  ok ?? range:init(>r, ? a, b);
  log.b(ok);// false 
  
  ok ?? range:init(>r, ? b, ? a);
  log.b(ok);// true 
 }

 { a := 32; b := -23 }

}.

Разрешения

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

 proc example3(>out []int) (ok bool) [ 
 post:
  allow uninit (out)
 ] {
  var ( i int )
  ok := false;
  if (ok)
    for (i := 0; i < len(out); i += 1)
      out[i] := len(out) - i
    end
  end
 }

Разрешение на неначализированность выходного параметра после вызова процедуры позволено, если

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

Разрешение на неначализированность входного или ссылочного параметра после вызова процедуры позволено, если

1. есть входной или ссылочный параметр без возможности неначализированности

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

Для входных и ссылочных параметров есть разрешение на неиспользование — allow unuse name, что может быть необходимо для соблюдения сигнатуры, например, для совместимости.

Полнота требований

Наличие явных требований к параметрам в объявлении ещё не означает, что они полны, то есть не составлены по принципу «лучше, чем ничего». Для указания, что требования исчерпывающие следует использовать двойные прямоугольные скобки.

func add3(a, b int) (sum int) [[
 ! min(int) <= a + b <= max(int)
post:
 ! sum = a + b
]] {
 // переполнение невозможно при выполнении предусловий
 sum := a + b
}

Неявные требования и их отсутствие

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

func add1(a, b int) (sum int) {/* Законно предполагать, что add1 вызывается
   с параметрами, не вызывающими переполнение, но и гарантий этого нет */ 
 sum := a + b // поэтому нужен контроль во время выполнения
}

func add2(a, b int) (sum int) [[]] {
 // Здесь очевидно, что возможно переполнение, так как a и b — любые
 sum := a + b
}