NDLI: Specifying and Proving Object-oriented Programs Specifying and Proving Object-oriented Programs

Please wait, while we are loading the content...

Specifying and Proving Object-oriented Programs Specifying and Proving Object-oriented Programs

Content Provider	CiteSeerX
Author	Fleck, A. C.
Abstract	This paper develops a new approach to the specification of object behavior. It utilizes an algebraic framework for precise specifications that can provide a basis for the verification of an implementation. These are abstract specifications that express behavior that is dependent on the local store without assuming an explicit configuration of instance variables. The conceptual basis for this new approach is to focus on behavior exclusively from the perspective of sequences of messages rather than that of individual messages. The local store of an object means that the effect of sending the same message may differ from one time to the next. This history-sensitive character is the central feature distinguishing state dependent object classes and purely functional abstract data types. The means by which this sequence outlook can be formally modeled is the main point of the paper. To substantiate the viability of the technique, an illustrative specification is presented. This specification shows that the essential properties of an object class can be captured without imposing a structure on the object’s state representation. To illustrate this, two implementations with highly contrasting state representations are shown, and indications are given of how the specification can be used to prove each is correct.
File Format	PDF
Access Restriction	Open
Subject Keyword	Object-oriented Program Specifying Object-oriented Program Local Store State Representation Illustrative Specification State Dependent Object Class Object Behavior Individual Message Precise Specification Algebraic Framework Essential Property Sequence Outlook Object Class History-sensitive Character Functional Abstract Data Type Object State Representation Instance Variable Conceptual Basis Main Point Abstract Specification Explicit Configuration Central Feature
Content Type	Text
Resource Type	Article

Central Library (ISO-9001:2015 Certified)
Indian Institute of Technology Kharagpur
Kharagpur, West Bengal, India | PIN - 721302

See location in the Map
03222 282435
Mail: support@ndl.gov.in

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