Ada "and" versus "and then": when does the difference matter in an if statement?

and is an ordinary operator: both operands are evaluated, in an order the language does not specify, and then combined. So Buffer (Index) is evaluated even when the range test is False, and the index check fails. and then is a short-circuit control form: the right operand is evaluated only if the left one is True. or else likewise evaluates the right side only if the left is False.

Your line should be if Index in Buffer'Range and then Buffer (Index) = 0 then.

The same pattern applies wherever the second test is only meaningful when the first passes: Ptr /= null and then Ptr.Value > 10, Count /= 0 and then Total / Count > Limit, S'Length > 0 and then S (S'First) = '#'. With plain and these can raise Constraint_Error from a null dereference, a division by zero or an index check.

A simple rule found in many style guides: write and then and or else for conditions in if and while, and keep and and or for computing Boolean values where both sides are always safe to evaluate.

Ada keeps both because and is a real operator with more uses than flow control. On modular types it is bitwise, for example Status and 16#0F# masks the low four bits, and on arrays of Boolean it works element by element. It can also be overloaded for your own types, which the short-circuit forms cannot.

Making the evaluation explicit is a deliberate design choice: the reader can see from the text whether the right-hand side is conditional.

Two details worth knowing. Ada does not let you mix different logical operators without parentheses: A and then B or else C is a syntax error and must be written (A and then B) or else C, so there is no precedence to remember.

And if the right operand is a function with a side effect, and always calls it while and then may skip it. If you want both validation functions to run and report, plain and is the correct choice; otherwise avoid side effects in conditions altogether.

The distinction matters in contracts too. A precondition such as Pre => Index in Table'Range and then Table (Index) > 0 must itself be free of run-time errors, and GNATprove checks that. Written with and, the tool reports that the index check in the second operand might fail, because nothing guarantees that the first operand holds when the second is evaluated. With and then the first part becomes a known fact for the second, and the check is proved.