Loop Fusion – преобразование программы для объединения нескольких последовательных петель в одну – было изучено в основном для оптимизации компилятора. В работе предлагается новая стратегия объединения циклов, которая может объединить любые петли, даже петли с зависимостью данных. Показано, что это полезно для программы проверки, потому что может упростить инварианты цикла. Суть цикла слияния заключается в следующем: если состояние после первого цикла было известно, два тела цикла могут быть вычислены одновременно, независимо от данных путем переименования переменных программы. Loop Fusion создает программу, которая угадывает неизвестное состояние после первого цикла, недетерминированно выполняет слитый цикл, в котором переменные переименовываются, сравнивает угаданное состояние и состояние, фактически вычисленное слитой петлей, и, если они не совпадают, расходится. Последние два шага, сравнение и расхождение, имеют решающее значение для сохранения частичной корректности. Подход «предположи и допусти» назван так потому, что в дополнение к первому шагу (предположи), последние два шага могут быть выражены псевдоинструкцией «допусти», которая используется в проверке программы.
Loop Fusion – Converting a program to combine multiple consecutive loops into one – has been studied mainly for compiler optimization. The paper proposes a new strategy for combining loops, which can combine any loops even loops with data dependency. It is shown that this is useful for the verification program, because it can simplify cycle invariants. The essence of the merge cycle is as follows: if the state after the first cycle was known, two bodies of the cycle can be calculated simultaneously, regardless of the data by renaming the program variables. Loop Fusion creates a program that guesses an unknown state after the first cycle, non-deterministically executes a merged cycle in which variables are renamed, compares the guessed state and the state actually calculated by the merged loop, and, if they do not match, diverges. The last two steps of the comparison and the discrepancy are crucial for maintaining partial correctness. The «suppose and allow» approach is so named because, in addition to the first step (suppose), the last two steps can be expressed by the «allow» pseudo-instruction used in program verification.
The authors declare that there are no conflicts of interest present.