Loop termination - Loop invariant
As mentioned in the comments, it depends on whether you care about partial correctness or total correctness.

Partial correctness requires that, if the program starts from any state satisfying the preconditions, and if the program terminates in a final state, then such final state satisfies the postcondition.

Total correctness requires that, if the program starts from any state satisfying the preconditions, then the program terminates in a final state, which satisfies the postcondition.

Only total correctness requires termination, partial correctness does not.

The Hoare logic rules for program statements are roughly the same, except for while loops. In partial correctness, the while rule requires to find a suitable invariant property. In total correctness, the rule requires both the invariant property and the variant: this is a strictly decreasing, natural valued function of the state (roughly, providing an upper bound on the number of loops).

If your rules have no variant, but only deal with the invariant, they are meant to be used to prove partial correctness, only.