Why isn't variable 'result' always declared?

Question

I am working with pseudocode taken from Exploration Tools (section "Arm A64 Instruction Set Architecture", button "Download XML").

bits(16) BFSub(bits(16) op1, bits(16) op2, FPCRType fpcr, boolean fpexc)

    FPRounding rounding = FPRoundingMode(fpcr);
    boolean done;
    bits(32) result;

    bits(32) op1_s = op1 : Zeros(16);
    bits(32) op2_s = op2 : Zeros(16);
    (type1,sign1,value1) = FPUnpack(op1_s, fpcr, fpexc);
    (type2,sign2,value2) = FPUnpack(op2_s, fpcr, fpexc);

    (done,result) = FPProcessNaNs(type1, type2, op1_s, op2_s, fpcr, fpexc);

Here we see that result is declared as bits(32) result.

bits(N) FPAdd(bits(N) op1, bits(N) op2, FPCRType fpcr, boolean fpexc)

    assert N IN {16,32,64};
    rounding = FPRoundingMode(fpcr);

    (type1,sign1,value1) = FPUnpack(op1, fpcr, fpexc);
    (type2,sign2,value2) = FPUnpack(op2, fpcr, fpexc);

    (done,result) = FPProcessNaNs(type1, type2, op1, op2, fpcr, fpexc);

Here we see that result is not declared. Why? Is it a bug?

I use version 2022-09. But version 2023-03 has the same issue.

Here is the full path to the file:

ISA_A64_xml_A_profile-2022-09/ISA_A64_xml_A_profile-2022-09/xhtml/shared_pseudocode.html

Answer 1

Repeat to yourself: "It's pseudo-code, I should really just relax :)

Usually we don't expect pseudocode to follow any particular formal grammar or semantics, so long as the intended meaning is clear enough to readers. However, in this case, ARM went kind of overboard in designing their pseudocode, so that it actually does approach an actual language, whose rules are in Section K16 of the Architecture Reference Manual. This language is statically typed, but it includes implicit declaration with type inference.

Specifically, in K16.3.1 we have:

A variable can be assigned to without an explicit declaration. The variable implicitly has the type of the assigned value.

And for tuples specifically, K16.3.8 has:

The general principle that types can be implied by an assignment extends to implying the type of the elements in the tuple.

Since FPProcessNaNs is defined with the signature

(boolean, bits(N)) FPProcessNaNs(FPType type1, FPType type2, bits(N) op1, bits(N) op2, FPCRType fpcr)

this means that the line

 (done,result) = FPProcessNaNs(type1, type2, op1, op2, fpcr, fpexc);

implicitly declares result as having type bits(N). Here, N is the same N as in the type of the op1,op2 arguments, which is in fact the same N used within FPAdd.

So in short, the code is well-formed and behaves the same as if bits(N) result; had been declared earlier in FPAdd.