A Mean Value Calculus based formal method is provided in this report
to specify and verify the steam-boiler control problem raised by
J.-R. Abrial[1] for Dagstuhl seminar. In addition to specifying safety
property, emphasis is put on capturing non-functional requirements
such as performance and optimization. Some formal design techniques
about finding an optimal implementation conforming to the system
specification are also discussed.