Does a do-while loop suffice for Turing-completeness?

I know that, in imperative programming languages, a while-do loop is sufficient as a control flow construct to make the language Turing-complete (as far as control flow goes - of course we also need unbounded memory and certain operators...). The gist of my question is: does a do-while loop have the same computational power as a while-do loop? In other words, can a language be Turing-complete if it's impossible to skip instructions entirely.

I realise that some of the semantics here could be a bit ambiguous, so let me phrase the actual question with a specific example:

Brainfuck (BF) is a Turing tarpit where the only control flow is a while-do loop, denoted as [...] (there is a complete language spec at the bottom of the question, in case you're not familiar with Brainfuck). Let's define a new language BF*, where ,.+-<> have the same semantics as in BF, but instead of [] we have {} which denotes a do-while loop. That is, the only difference to BF is that every loop is executed at least once before further iterations can be skipped.

Is BF Turing-complete? If it is, I'd be interested in how I could translate BF to BF. If it isn't, how do I prove that?

Some observations of my own:

• Not every BF program can be translated into BF. For instance, it's impossible to write a program in BF which may or may not read or print a value - if the program potentially prints one or more values, it will always print at least one. However, there might be a Turing-complete subset of BF which can be translated to BF*.

• We cannot simply translate [f] (where f is some arbitrary, Brainfuck program consisting only of +-[]<>) to f-1{f} (in an attempt to cancel the effect of the first iteration), because a) not every computable function has a computable inverse and b) even if it did, f-1 wouldn't necessarily have fewer loops than f so applying this step recursively isn't guaranteed to terminate in the first place.

Here is a quick overview over the Brainfuck lan

I don't know Brainfuck so you'll have to do some translation from my pseudocode. But, assuming that Brainfuck behaves sensibly (ha!), everything below should apply.

do-while is equivalent to while-do. do X while Y is equivalent to X; while Y do X and, assuming you have conditionals, while Y do X is equivalent to if Y then (do X while Y).

Life is a bit harder if you don't have conditionals. If you have while-do, you can simulate if Y then X using something like this:

B := true
while (Y and B) do
    X
    B := false
endwhile

But what if you only have do-while? I claim that the following simulates if Y then X, assuming that X terminates given the current value of the variables. (This isn't guaranteed: the program if y=0 then loopforever terminates if y != 0, even though X loops for any value of the variables). Let V1, ..., Vn be the variables modified by X and let X' be X modified so that it uses Vi' instead of Vi for each of those variables. swap(A,B) denotes the obvious code that swaps the variables A and B.

V1' := V1; ...; Vn' := Vn
V1'' := V1; ...; Vn'' := Vn
C := 0
do
    X'
    swap (V1',V1''); ...; swap (Vn',Vn'')
    C := C+1
while Y and C<2
V1 := V1'; ...; Vn := Vn'

The idea is the following. First, suppose that Y is false. We simulate doing X once, and store the results in V1'', ..., Vn''; V1', ..., Vn' hold the original values of V1, ..., Vn. Then, we assign V1 := V1'; ...; Vn := Vn', which does nothing. So, if Y is false, we've done nothing. Now, suppose that Y is true. We'll now simulate X twice, storing the results in both the "primed" and "double-primed" variables. So, now, the assignments at the end of the loop have the effect that X was computed once. Note that Y only depends on the "unprimed" variables, so its value is not affected by running the loop repeatedly.

OK, so what if X might not terminate for the current value of the variables? (Thanks to Martin Ender for pointing out this possibility.)
In that case, we need to simulate X instruction-by-instruction, using similar ideas to those above. Each instruction definitely terminates so we can use the if simulation above to do instruction decoding, along the lines of "If the opcode is foo, do this; if it's bar, do that; ...". So, now, we use a loop to iterate through the instructions of X, using an instruction pointer and so on so that we know which instruction to execute next. At the end of each iteration of the loop, check Y and check whether X has halted yet. If Y is false, the swapping technique allows us to undo the effects of X's first instruction.

StackExchange Computer Science Q#47603, answer score: 10