Ignore:
Timestamp:
Feb 20, 2014, 11:43:47 AM (6 years ago)
Author:
mulligan
Message:

de-Tristram Shandefied the opening paragraph

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/fopara2013/fopara13.tex

    r3450 r3451  
    111111
    112112%\paragraph{Problem statement.}
    113 Computer programs can be specified with both
    114 functional constraints (what a program must do) and non-functional constraints
    115 (what resources---time, space, etc.---the program may use).  In the current
    116 state of the art, functional properties are verified for high-level source code
    117 by combining user annotations (e.g. preconditions and invariants) with a
    118 multitude of automated analyses (invariant generators, type systems, abstract
    119 interpretation, theorem proving, and so on). By contrast, many non-functional properties
    120 are generally checked on low-level object code,
     113Programs can be specified with both
     114functional constraints (what the program must do) and non-functional constraints (what time, space or other resources the program may use).  In the current
     115state of the art, functional properties are verified
     116by combining user annotations---preconditions, invariants, and so on---with a
     117multitude of automated analyses---invariant generators, type systems, abstract
     118interpretation, theorem proving, and so on---on the program's high-level source code.
     119By contrast, many non-functional properties
     120are verified using analyses on low-level object code,
    121121%\footnote{A notable
    122122%  exception is the explicit allocation of heap space in languages like C, which
    123123%  can be handled at the source level.}
    124 but also demand information
    125 about high-level functional behaviour that must somehow be reconstructed.
     124but these analyses may then need information
     125about the high-level functional behaviour of the program that must then be reconstructed.
    126126
    127127This situation presents several problems: 1) it can be hard to infer this
Note: See TracChangeset for help on using the changeset viewer.