Difference between revisions of "WG211/M11Herrmann"
(Created page with "I will present a new aspect of software engineering which involves the automatic derivation of program properties during generation of low-level programs (assembly code for an a...") |
|||
| Line 8: | Line 8: | ||
I am convinced that efforts are better spent in developing analyses together with | I am convinced that efforts are better spent in developing analyses together with | ||
the program generation or interactively with the manual design process. | the program generation or interactively with the manual design process. | ||
| − | The predominant development approach in practice is first | + | The predominant development approach in practice is to first write a program and then |
| − | to | + | to profile and change it if it does not fit the expectations. At the other end of the |
scale is the approach of using a programming language with dependent types, which | scale is the approach of using a programming language with dependent types, which | ||
would provide even strong formal guarantees but also slows down the program | would provide even strong formal guarantees but also slows down the program | ||
development process due to the need to find appropriate proofs at many places. | development process due to the need to find appropriate proofs at many places. | ||
I believe that the approach of combining generation with analysis can unite both a | I believe that the approach of combining generation with analysis can unite both a | ||
| − | rapid program development and an analysis which benefits from design knowledge. | + | rapid program development and an analysis which benefits from design knowledge |
| + | and can provide results which are parameterised, i.e. valid for an entire range of | ||
| + | control parameters. | ||
Revision as of 18:48, 3 June 2012
I will present a new aspect of software engineering which involves the automatic derivation of program properties during generation of low-level programs (assembly code for an abstract machine) from high-level specifications (such as SQL). For certain properties in dedicated application areas, such as worst-case execution time for embedded systems, much effort has been spent to adapt or instrument programs to fit the need of existing analysis tools, but this can only assist such tools concerning aspects they are already prepared for. I am convinced that efforts are better spent in developing analyses together with the program generation or interactively with the manual design process. The predominant development approach in practice is to first write a program and then to profile and change it if it does not fit the expectations. At the other end of the scale is the approach of using a programming language with dependent types, which would provide even strong formal guarantees but also slows down the program development process due to the need to find appropriate proofs at many places. I believe that the approach of combining generation with analysis can unite both a rapid program development and an analysis which benefits from design knowledge and can provide results which are parameterised, i.e. valid for an entire range of control parameters.
