Compile time preparations for run time scheduling in monitors

High level programming language constructs are proposed for scheduling of concurrent operations on a shared variable. Proof rules are given that can be used to check if an adequate scheduling can be prepared from the program text. The basis for the constructs is the condition that must be fulfilled before an operation on a shared variable is performed (the precondition of the operation) and what can be proved to hold when an operation terminates (the postassertion of the operation).