How do I read this notation and what does it mean?

Question

The notation is ⊢P{Q}R. To give context, the notation is from a paper called "An Axiomatic Basis for Computer Programming". From what I know, the symbol ⊢ is used to show that something(B) is derivable from another(A); i.e A⊢B, or B is a partition of A.

Answer 1

See Hoare logic :

A Hoare triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form

$$\{ P \} C \{ Q \}$$

where $P$ and $Q$ are assertions and $C$ is a command. $P$ is named the precondition and $Q$ the postcondition: when the precondition is met, executing the command establishes the postcondition.

Ref to C.A.R. Hoare's An Axiomatic Basis for Computer Programming (1969) page 577 for the original notation: $P \{ Q \} R$.

And see footnote 1:

If $P \{ Q \} R$ can be proved in our formal system, we use the familiar logical symbol for theoremhood : $\vdash P \{ Q \} R$.

See Turnstile symbol for $\vdash$.