# Formalizing Transformation Rules between Similar Loop Constructs

I'm trying to understand and formalize the relationship between two similar but slightly different loop structures in different programming languages:

Example 1 (PHP):

do {
statement(s)
} while (condition);


Example 2 (LUA):

repeat
statement(s)
until condition


These loops differ in how they handle their conditions:

1. Example 1 continues as long as the condition is true, evaluating the condition after each iteration.
2. Example 2 continues until the condition becomes true, also evaluating the condition after each iteration.

The transformation between these loops can be described with this custom logical statement:

repeat S until(C) ⇔ do { S } while(!C)


Where S represents the statement(s) in the loop body, and C represents the condition.

My question is: Is there a more formal notation or system for expressing such transformations between different programming language constructs?

I was considering Hoare logic or Structural Operational Semantics, but both seem rather complex, and I cannot easily determine if I can use them.

I would be grateful for any guidance in the right direction.

New contributor
user2862893 is a new contributor to this site. Take care in asking for clarification, commenting, and answering. Check out our Code of Conduct.
• – D.W.
Commented Aug 1 at 7:23

Operational semantics is arguably the simplest way of formalizing the semantics of programming languages, especially imperative languages. If your goal is to write a formal proof that "do while" and "repeat until" are equally expressive, you should learn operational semantics. You will find it in most introductions to programming language theory.

For example, this Introduction to the semantics of programming languages seems pretty comprehensive, including also the mathematical prerequisites in its first chapter. It is linked at the bottom of the Wikipedia article on Operational semantics. Its subtitle mentions Structural operational semantics which is a particular flavor of operational semantics, but it doesn't matter what it's called exactly as long as you find adequate introductory material.

You won't define the semantics of PHP and Lua because those are too big to be practical to formalize. Instead you can define simple imperative languages featuring "do while" and "repeat until", with their operational semantics. You then define a translate function from one to the other, and prove that the result of translate simulates the original program. Here's a very quick sketch:

Definition:

translate(DO p WHILE c) = REPEAT translate(p) WHILE (translate(c))
(omitted: the rest of the definition of translate)


Theorem:
For any program p and states s and s', we have (p, s) -> s' if and only if (translate(p), s) -> s'.

To summarize: take an introductory class on the semantics of programming languages.