Explore the vast range of titles available.

This book – composed of two volumes – explores the syntactical constructs of the most common programming languages, and sheds a mathematical light on their semantics, providing also an accurate presentation of the material aspects that interfere with coding. Concepts and Semantics of Programming Languages 2 presents an original semantic model, collectively taking into account all of the constructs and operations of modules and classes: visibility, import, export, delayed definitions, parameterization by types and values, extensions, etc. The model serves for the study of Ada and OCaml modules, as well as C header files. It can be deployed to model object and class features, and is thus used to describe Java, C++, OCaml and Python classes. This book is intended not only for computer science students and teachers but also seasoned programmers, who will find a guide to reading reference manuals and the foundations of program verification.

From the Preface Ada's Legacy illustrates the depth and diversity of writers, thinkers, and makers who have been inspired by Ada Lovelace, the English mathematician and writer. The volume, which commemorates the bicentennial of Ada's birth in December 1815, celebrates Lovelace's many achievements as well as the impact of her life and work, which reverberated widely since the late 19th century. In the 21st century we have seen a resurgence in Lovelace scholarship, thanks to the growth of interdisciplinary thinking and the expanding influence of women in science, technology, engineering, and mathematics. Ada's Legacy is a unique contribution to this scholarship. Here, the editors present work on topics previously unknown to coexist in print: Ada's collaboration with Charles Babbage, the development of the Ada programming language, Ada's position in the Victorian and Steampunk literary genres, Ada's representation in and inspiration of contemporary art and comics, and Ada's continued relevance in discussions around gender and technology in the digital age. With the 200th anniversary of Ada Lovelace's birth on December 10, 2015, we believe that the timing is perfect to publish this collection. Because of its broad focus on subjects that reach far beyond the life and work of Ada herself, Ada's Legacy will appeal to readers who are curious about Ada's enduring importance in computing and the wider world. The idea for this book originated from the first academic conference of its kind, Ada Lovelace: An Interdisciplinary Conference Celebrating her Achievements and Legacy, which took place at Stevens Institute of Technology (Hoboken, New Jersey) on October 18, 2013, under the auspices of the Institute's College of Arts and Letters. The time was definitely right to bring this conference to Stevens, which was until 1971 a male-only school. By 1982, Stevens became the first major institute in the United States to implement a personal computer requirement for its students. Around this time, a pioneering technology project resulted in the networking of the entire Stevens campus, creating one of the nation's first intranets. Additionally, the recent development of undergraduate programs in the College of Arts and Letters, including Gender Studies as well as Science and Technology Studies, which strongly anchors women in STEM, clearly made Stevens well positioned to host a conference celebrating Lovelace's achievements and legacy. The conference brought together international scholars from across the disciplines to coincide with the week celebrating Ada Lovelace Day. Tremendous interest circulated in advance of the conference, particularly among computing history specialists and 19th-century literary scholars, and it escalated immediately following the proceedings. Tom Misa, director of the Charles Babbage Institute and a featured speaker at the conference, numbered chiefly among those who caught this interest. He envisioned the possibility for a book project to develop concrete examination of ideas inspired by the proceedings. The conference organizer, Robin Hammerman, and Andrew Russell, director of the College of Arts and Letters Science and Technology Studies program, enthusiastically agreed to collaborate as editors for this interdisciplinary collection. Many of the papers published in this volume first were presented at the conference in October 2013. We are pleased to acknowledge the supporters of that conference: Dr. Lisa Dolling, former Dean of the College of Arts & Letters at Stevens Institute of Technology, and Dr. George Korfiatis, Provost of Stevens Institute of Technology. The editors are grateful to Thomas J. Misa, Series Editor for ACM's History of Computing, for skillfully overseeing the development of this project from its inception to completion. We also are happy to thank Diane Cerra, Executive Editor at Morgan & Claypool Publishers, for her kind and capable attention to the production of this volume. And we are delighted that Sydney Padua graciously agreed to create original illustrations for Ada's Legacy.

The Ada programming language was created by the U.S. Department of Defense (DOD) nearly two decades ago to provide a general-purpose programming language for defense and commercial use, but has evolved into a niche solution for safety-critical systems, primarily in defense applications. Ada and Beyond presents an approach for the DOD to move beyond the debate over its policy that requires the use of Ada for all new software development. It describes the importance of the software engineering process and recommends to DOD mechanisms for more effective review of software development and improved collection of data on software project outcomes. The volume also analyzes the technical, empirical, and business cases for using Ada and other programming languages, makes recommendations regarding the appropriate conditions under which DOD should continue to require the use of Ada, and details activities that require funding by DOD in order for Ada to remain a viable programming language.

Unlike for conventional compilers for imperative programming languages such as C or ADA, no established methods for safeguarding artifacts generated by model-based code generators exist despite progress in the field of formal verification. Several test approaches dominate the engineering practice. This paper describes a general and tool-independent test architecture for code generators used in model-based development. We evaluate the effectiveness of our test approach by means of testing optimizations performed by the TargetLink code generator, a widely accepted and complex development tool used in automotive model-based development.

Sea erosion is a serious threat to life and property in coastal towns. The coastline of Ada Foah has been facing sea erosion and occasional flooding for several decades. This research investigated the socio-economic and environmental impacts of these geomorphic processes using social survey methods of data collection and shoreline change analysis. The main research tools used include questionnaire survey, interviews and Digital Shoreline Analysis System (DSAS) 4.2 software using extracted shorelines of 1926 ground survey sheet and 2008 Landsat ETM+ image to determine shoreline change between the periods. The research identified some environmental and socio-economic impacts of the sea erosion on the coastal community, and these include the destruction of coastal ecosystems and infrastructure such as offices of institutions, school blocks and roads. The ramifications of these problems include homelessness, unemployment and poverty, which compel victims to migrate. Results of shoreline change analysis indicate that, the Ada Foah shoreline has been receding since 1926 to date with a mean change in shoreline of 280.49 m and an average annual rate of 3.46 m/year. To protect the coastline from the battering sea, a sea defence project, comprising sand nourishment and the construction of groynes, is being undertaken.

We present functional dependencies , a convenient, formal, but high-level, specification format for a piece of procedural software (function). Functional dependencies specify the set of memory locations, which may be modified by the function, and for each modified location, the set of memory locations that influence its final value. Verifying that a function respects pre-defined functional dependencies can be tricky: the embedded world uses C and Ada, which have arrays and pointers. Existing systems we know of that manipulate functional dependencies, Caveat and SPARK, are restricted to pointer-free subsets of these languages. This article deals with the functional dependencies in a programming language with full aliasing. We show how to use a weakest pre-condition calculus to generate a verification condition for pre-existing functional dependencies requirements. This verification condition can then be checked using automated theorem provers or proof assistants. With our approach, it is possible to verify the specification as it was written beforehand. We assume little about the implementation of the verification condition generator itself. Our study takes place inside the C analysis framework Frama-C, where an experimental implementation of the technique described here has been implemented on top of the WP plug-in in the development version of the tool.

The article examines 'software fun' from the viewpoint of the role of methodologies in software history. Historically, (1950s), programming was a small-scale, problem-solving activity. There were few firm requirements. Programmers worked with prototypes and used them to extend their knowledge as they created new products. In doing this, they maximized fun. The author concludes that the software process optimization approaches of the past had their place, and perhaps they still do. The methodologized approaches that today's gurus favor also had, and continue to have, their place. But there's a huge gap between \"when tasks are small...\" and \"only valid for firm and stable requirements.\" The answer is a structured, object-oriented, knowledge-based prototyping paradigm based on formal specifications and proofs of correctness that combines the main features of composition and decomposition in a CASE environment using methodology-independent methods and visual programming in Ada

A language-based approach to deterministic execution debugging of concurrent Ada programs is presented. The approach is to define synchronization (SYN)-sequences of a concurrent Ada program in terms of Ada language constructs and to replay such SYN-sequences without the need for system-dependent debugging tools. It is shown how to define a SYN-sequence of a concurrent Ada program in order to provide sufficient information for deterministic execution. It is also shown how to transform a concurrent Ada program P so that the SYN-sequences of previous executions of P can be replayed. This transformation adds an Ada task to P that controls program execution by synchronizing with the original tasks in P. A brief description is given of the implementation of tools supporting deterministic execution debugging of concurrent Ada programs.< >

Among formal methods, the deductive verification approach allows establishing the strongest possible formal guarantees on critical software. The downside is the cost in terms of human effort required to design adequate formal specifications and to successfully discharge the required proof obligations. To popularize deductive verification in an industrial software development environment, it is essential to provide means to progressively transition from simple and automated approaches to deductive verification. The SPARK environment, for development of critical software written in Ada, goes towards this goal by providing automated tools for formally proving that some code fulfills the requirements expressed in Ada contracts. In a program verifier that makes use of automatic provers to discharge the proof obligations, a need for some additional user interaction with proof tasks shows up: either to help analyzing the reason of a proof failure or, ultimately, to discharge the verification conditions that are out-of-reach of state-of-the-art automatic provers. Adding interactive proof features in SPARK appears to be complicated by the fact that the proof toolchain makes use of the independent, intermediate verification tool Why3, which is generic enough to accept multiple front-ends for different input languages. This paper reports on our approach to extend Why3 with interactive proof features and also with a generic client-server infrastructure allowing integration of proof interaction into an external, front-end graphical user interface such as the one of SPARK.