Denotational semantics of IMP While

61 Views Asked by At

I know that the denotational semantics of the IMP while loop is the least fixed point of $\mathcal{F}:(State \rightharpoondown State) \rightarrow (State \rightharpoondown State)$, written as: $[\![ while(b) \quad s]\!] = fix(\mathcal{F})$, where $fix$ is the least fixed-point. And that the fixed-points of $\mathcal{F}$ are elements $(State \rightharpoondown State)$. But how do I know that it's the least-fixed point? And how would I describe all the fixed points of $\mathcal{F}$ associated to the IMP while loop?