Difference between revisions of "WG211/M11Herrmann"
| Line 1: | Line 1: | ||
I will present a new aspect of software engineering which involves the automatic | I will present a new aspect of software engineering which involves the automatic | ||
| − | derivation of program properties during generation of low-level programs (assembly | + | derivation of parameterised program properties during generation of low-level programs |
| − | code for an abstract machine) from high-level specifications (such as SQL). | + | (such as assembly code for an abstract machine) from high-level specifications (such as SQL). |
For certain properties in dedicated application areas, such as worst-case | For certain properties in dedicated application areas, such as worst-case | ||
execution time for embedded systems, much effort has been spent to adapt or | 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 | instrument programs to fit the need of existing analysis tools, but this can only | ||
| − | assist such tools concerning aspects they are already prepared for. | + | assist such tools concerning aspects they are already prepared for. In industrial |
| − | I | + | settings where manual instrumentation or code adaptation would be infeasible due to |
| − | the | + | the program size, severe limitations such as constant upper bounds on loops are imposed |
| + | before carrying out a completely automatic worst-case execution time analysis. | ||
| + | I think that it could be very useful to derive program properties during the generation including | ||
| + | as many design decisions as possible, maybe interactively guided by a manual design process. | ||
The predominant development approach in practice is to first write a program and then | 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 | + | to test it on concrete data, profile it and change it if it does not fit the expectations. |
| − | scale is the approach of using a programming language with dependent types, which | + | At the other end of the scale is the approach of using a programming language with dependent |
| − | would provide even strong formal guarantees but also slows down the program | + | types, which would provide even strong formal guarantees by an independent instance (the type checker) |
| − | development process due to the need to find appropriate proofs at many places. | + | but also slows down the program development process due to the need to find appropriate proofs at |
| − | I believe that the approach of combining generation with analysis can | + | many places. I believe that the approach of combining generation with analysis can establish both a |
| − | rapid program development and an analysis which benefits from design knowledge | + | rapid program development and provide an analysis which benefits from design knowledge |
| − | and | + | and delivers results which are parameterised, i.e. valid for an entire range of values for |
| − | control parameters. | + | important control parameters, such as the size of the problem instance. |
Latest revision as of 19:08, 3 June 2012
I will present a new aspect of software engineering which involves the automatic derivation of parameterised program properties during generation of low-level programs (such as 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. In industrial settings where manual instrumentation or code adaptation would be infeasible due to the program size, severe limitations such as constant upper bounds on loops are imposed before carrying out a completely automatic worst-case execution time analysis. I think that it could be very useful to derive program properties during the generation including as many design decisions as possible, maybe interactively guided by a manual design process. The predominant development approach in practice is to first write a program and then to test it on concrete data, profile it 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 by an independent instance (the type checker) 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 establish both a rapid program development and provide an analysis which benefits from design knowledge and delivers results which are parameterised, i.e. valid for an entire range of values for important control parameters, such as the size of the problem instance.
