NDLI: Provably correct derivation of algorithms using FermaT

Content Provider	Springer Nature Link
Author	Ward, Martin Zedan, Hussein
Copyright Year	2013
Abstract	The transformational programming method of algorithm derivation starts with a formal specification of the result to be achieved, plus some informal ideas as to what techniques will be used in the implementation. The formal specification is then transformed into an implementation, by means of correctness-preserving refinement and transformation steps, guided by the informal ideas. The transformation process will typically include the following stages: (1) Formal specification (2) Elaboration of the specification, (3) Divide and conquer to handle the general case (4) Recursion introduction, (5) Recursion removal, if an iterative solution is desired, (6) Optimisation, if required. At any stage in the process, sub-specifications can be extracted and transformed separately. The main difference between this approach and the invariant based programming approach (and similar stepwise refinement methods) is that loops can be introduced and manipulated while maintaining program correctness and with no need to derive loop invariants. Another difference is that at every stage in the process we are working with a correct program: there is never any need for a separate “verification” step. These factors help to ensure that the method is capable of scaling up to the development of large and complex software systems. The method is applied to the derivation of a complex linked list algorithm and produces code which is over twice as fast as the code written by Donald Knuth to solve the same problem.
Starting Page	993
Ending Page	1031
Page Count	39
File Format	PDF
ISSN	09345043
Journal	Formal Aspects of Computing
Volume Number	26
Issue Number	5
e-ISSN	1433299X
Language	English
Publisher	Springer London
Publisher Date	2013-10-22
Publisher Place	London
Access Restriction	Subscribed
Subject Keyword	Transformational programming Formal methods Software development Algorithm derivation FermaT WSL Math Applications in Computer Science Theory of Computation Computational Mathematics and Numerical Analysis
Content Type	Text
Resource Type	Article
Subject	Theoretical Computer Science Software

Sl.	Authority	Responsibilities	Communication Details
1	Ministry of Education (GoI), Department of Higher Education	Sanctioning Authority	https://www.education.gov.in/ict-initiatives
2	Indian Institute of Technology Kharagpur	Host Institute of the Project: The host institute of the project is responsible for providing infrastructure support and hosting the project	https://www.iitkgp.ac.in
3	National Digital Library of India Office, Indian Institute of Technology Kharagpur	The administrative and infrastructural headquarters of the project	Dr. B. Sutradhar bsutra@ndl.gov.in
4	Project PI / Joint PI	Principal Investigator and Joint Principal Investigators of the project	Dr. B. Sutradhar bsutra@ndl.gov.in Prof. Saswat Chakrabarti will be added soon
5	Website/Portal (Helpdesk)	Queries regarding NDLI and its services	support@ndl.gov.in
6	Contents and Copyright Issues	Queries related to content curation and copyright issues	content@ndl.gov.in
7	National Digital Library of India Club (NDLI Club)	Queries related to NDLI Club formation, support, user awareness program, seminar/symposium, collaboration, social media, promotion, and outreach	clubsupport@ndl.gov.in
8	Digital Preservation Centre (DPC)	Assistance with digitizing and archiving copyright-free printed books	dpc@ndl.gov.in
9	IDR Setup or Support	Queries related to establishment and support of Institutional Digital Repository (IDR) and IDR workshops	idr@ndl.gov.in

Provably-correct hardware compilation tools based on pass separation techniques

Limits of formal methods

Practice-oriented courses in formal methods using VDM++

Towards a linear algebra of programming

Using a formal specification contractually

A CSP model of Eiffel’s SCOOP

Deriving dense linear algebra libraries

Trace-based derivation of a scalable lock-free stack algorithm

Assumption propagation through annotated programs

Provably correct derivation of algorithms using FermaT

Similar Documents

Provably-correct hardware compilation tools based on pass separation techniques

Limits of formal methods

Practice-oriented courses in formal methods using VDM++

Towards a linear algebra of programming

Using a formal specification contractually

A CSP model of Eiffel’s SCOOP

Deriving dense linear algebra libraries

Trace-based derivation of a scalable lock-free stack algorithm

Assumption propagation through annotated programs

Provably correct derivation of algorithms using FermaT