A Study in Formal Specifications With Application to Price Calculations in the Power Market
Maria Gramner · KTH Publication Database DiVA (KTH Royal Institute of Technology) · 2015
The world today is getting more and more dependent on digital technique, and errors in software can be expensive or hard to fix. Because of this, it is more important than ever to have a reliable way of making sure that developed programs work correctly. This thesis will give an introduction to formal specifications and examine the possible usefulness of one for a price calculating program concerning electricity contracts. Some background information on formal specifications will be presented along with a description of some of the different available techniques for writing one. Furthermore, a model-based specification in the language Z will be developed, and the study will show that this approach to program correctness can be useful for, among other things, programs for the financial domain.