Programming in stages Programming in stages
P
r
o
g
r
a
m
m
i
n
g
i
n
s
t
a
g
e
s
K. Rustan M. Leino
Principal Researcher
Research in Software Engineering (RiSE), Microsoft Research, Redmond
Visiting Professor
Department of Computing, Imperial College London
VSSE 2014, 5 Apr 2014, Grenoble, France
Software engineering
Costly
Two programming problems
Development of software
Maintenance of software
Evolving program complexity
Destructive maintenance vs. staged development
Not just a problem with evolution, but also with initial conception
Example: developing a BDD package
Simple data structures
Reductions
Hash-consing
Caches for performance
Garbage collection and node reuse
Evaluate variable ordering and dynamic change it
Etc.
Helping the developer
Programming language is the developer’s most important tool
Capture more of the design in the program text
Present details at the right time
a)
Procedural abstraction
b)
Modules and interfaces
Parnas’s decomposition guide, 1972
c)
Subclassing
d)
Aspects
Cut points, advice
Not enough focus on correctness and reasoning
e)
Refinement
Specification and program are introduced in stages
Program refinement
Ideas
Edsger W. Dijkstra, 1968
Niklaus Wirth, 1971
Formalization
Ralph Back, 1978
Use and extensions
Numerous people, 1980s
Language design
Gries, Prins, Volpano, mid and late 1980s
Doug Smith: KIDS, 1980s
Jean-Raymond Abrial: the B method, Event-B, 1990s and 2000s
Dafny
Programming language and system designed with
reasoning
in mind
Research tool
Interplay between language, verifier, compiler, IDE
Push the envelope in automatic verification
Try combination of language features
Applications
Ironclad (MSR), ExpressOS (UIUC)
Teaching
Imperial College London, Rice U., Caltech, Moscow State U.,
KSU, NUI Maynooth, ETH Zurich, UW, U. Iowa, Koç U., UNSW,
Princeton, CMU, Eindhoven TU, Ohio State U.,
FCT Universidade
Nova de Lisboa, U.
Basque Country, U. Southhampton, …
Refinement in Dafny
Reduction of non-determinism
Superposition
No direct support for data refinement
Use superpositions and ghost variables instead
Refinement is provided as a
structuring device
Refinements have to be anticipated
“Shims” already in place
Joint work with Jason Koenig
Demos
Specification
Model
implementation
Simple
implementation
Optimized
implementation
Client
M0:
M1:
M2:
M3:
Optimized
client
Verify
Compile
Compile
Conclusions
Preserve, in the program text, more design decisions and the design
evolution
Refinement allows programs to be structured in
stages
Layer the complexity, not just the call graph
Language design for refinement
What constructs to use?
How to make more independent of formality?
Evaluation
Is the mental overhead really lower?
Is maintenance really cheaper this way?
In software engineering, the process of programming unfolds in stages, addressing evolving program complexity, maintenance challenges, and program refinement. Key aspects include helping developers with programming languages, presenting details effectively, and refining programs over time. With a focus on continual improvement and structured development, programming in stages enhances software design and evolution.
Download Presentation
Please find below an Image/Link to download the presentation.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.If you encounter any issues during the download, it is possible that the publisher has removed the file from their server.
You are allowed to download the files provided on this website for personal or commercial use, subject to the condition that they are used lawfully. All files are the property of their respective owners.
The content on the website is provided AS IS for your information and personal use only. It may not be sold, licensed, or shared on other websites without obtaining consent from the author.
E N D
Presentation Transcript
Programming in stages Programming in stages K. Rustan M. Leino Principal Researcher Research in Software Engineering (RiSE), Microsoft Research, Redmond Visiting Professor Department of Computing, Imperial College London VSSE 2014, 5 Apr 2014, Grenoble, France
Software engineering Costly Two programming problems Development of software Maintenance of software
Evolving program complexity Destructive maintenance vs. staged development Not just a problem with evolution, but also with initial conception
Example: developing a BDD package Simple data structures Reductions Hash-consing Caches for performance Garbage collection and node reuse Evaluate variable ordering and dynamic change it Etc.
Helping the developer Programming language is the developer s most important tool Capture more of the design in the program text
Present details at the right time a) Procedural abstraction b) Modules and interfaces Parnas s decomposition guide, 1972 c) Subclassing d) Aspects Cut points, advice Not enough focus on correctness and reasoning e) Refinement Specification and program are introduced in stages
Program refinement Ideas Edsger W. Dijkstra, 1968 Niklaus Wirth, 1971 Formalization Ralph Back, 1978 Use and extensions Numerous people, 1980s Language design Gries, Prins, Volpano, mid and late 1980s Doug Smith: KIDS, 1980s Jean-Raymond Abrial: the B method, Event-B, 1990s and 2000s
Dafny Programming language and system designed with reasoning in mind Research tool Interplay between language, verifier, compiler, IDE Push the envelope in automatic verification Try combination of language features Applications Ironclad (MSR), ExpressOS (UIUC) Teaching Imperial College London, Rice U., Caltech, Moscow State U., KSU, NUI Maynooth, ETH Zurich, UW, U. Iowa, Ko U., UNSW, Princeton, CMU, Eindhoven TU, Ohio State U., FCT Universidade Nova de Lisboa, U. Basque Country, U. Southhampton,
Refinement in Dafny Joint work with Jason Koenig Reduction of non-determinism Superposition No direct support for data refinement Use superpositions and ghost variables instead Refinement is provided as a structuring device Refinements have to be anticipated Shims already in place
M0: Verify Demos M1: Client Compile Optimized client M2: Compile M3:
Conclusions Preserve, in the program text, more design decisions and the design evolution Refinement allows programs to be structured in stages Layer the complexity, not just the call graph Language design for refinement What constructs to use? How to make more independent of formality? Evaluation Is the mental overhead really lower? Is maintenance really cheaper this way?
