Why are there strange pragmas for Locking levels and other properties?

The Trestle (ui library) interfaces contain Locking level pragmas. The base interfaces (libm3 library) contain SPEC pragmas. These are not processed by the compiler. Instead the Extended Static Checker, currently under development at DEC SRC, will report on problems detected based on the program content and the information specified in these pragmas [ESC]. The Extended Static Checker is not yet available, it may be some time in the future.