Understanding the thought processes of students as they progress from initial (incorrect) answers toward correct answers is a challenge for instructors, both in this pandemic and beyond. This paper presents a general network visualization learning analytics system that helps instructors to view a sequence of answers input by students in a way that makes student learning progressions apparent. The system allows instructors to study individual and group learning at various levels of granularity. The paper illustrates how the visualization system is employed to analyze student responses collected through an intervention. The intervention is BeginToReason, an online tool that helps students learn and use symbolic reasoning-reasoning about code behavior through abstract values instead of concrete inputs. The specific focus is analysis of tool-collected student responses as they perform reasoning activities on code involving conditional statements. Student learning is analyzed using the visualization system and a post-test. Visual analytics highlights include instances where students producing one set of incorrect answers initially perform better than a different set and instances where student thought processes do not cluster well. Post-test data analysis provides a measure of student ability to apply what they have learned and their holistic understanding.

To develop code that meets its specification and is verifiably correct, such as in a software engineering course, students must be able to understand formal contracts and annotate their code with assertions such as loop invariants. To assist in developing suitable instructor and automated tool interventions, this research aims to go beyond simple pre- and post-conditions and gain insight into student learning of loop invariants involving objects. As students develop suitable loop invariants for given code with the aid of an online system backed by a verification engine, each student attempt, either correct or incorrect, was collected and analyzed automatically, and catalogued using an iterative process to capture common difficulties. Students were also asked to explain their thought process in arriving at their answer for each submission. The collected explanations were analyzed manually and found to be useful to assess their level of understanding as well as to extract actionable information for instructors and automated tutoring systems. Qualitative conclusions include the impact of the medium.

We present results in automating the analysis of student verbalizations in online learning environments, using an existing online tool designed to teach students to reason analytically about code as an example. The new extension captures "think-aloud'' data as students work through code reasoning activities. The data is recorded and transcribed automatically and used as input to a natural language processing / machine learning system designed to identify specific student attitudes (e.g., uncertain), behaviors (e.g., guessing), and difficulties (e.g., concept misunderstandings). We present the design and implementation of the tool, an analysis of its transcription accuracy, and an evaluation of its utility in identifying characteristics of student learning.

You develop a plan for testing the prototype for a new learning strategy in your class or across institutions. How can you ensure that your plan is clearly understood by reviewers and the managing NSF program officer? What goes through the reviewer's mind once a proposal is submitted? What prompts one proposal to be recommended for funding but another declined? Close examination of the panel review process can inform proposal writing and ensure that reviewers will understand an idea, identify its merit, and value a PI's vision of how the work will broaden participation in STEM education. This workshop steps through the NSF proposal review process from submission of proposal to award or decline, touching on NSF intellectual merit and broader impact criteria, mapping the project pipeline to appropriate evaluation. Participants gain insight into writing a good review and improving one's own proposal writing. For further information and travel support see: https://people.cs.clemson.edu/~etkraem/UPCSEd/. Laptops recommended.

Several research studies have shown the benefits of code tracing to promote student understanding of program behavior. While code tracing on specific input values is a useful starting point, students ultimately need to be able to reason rigorously and logically about the correctness of their code on all (i.e., arbitrary) inputs. Otherwise, they may make false generalizations and may achieve only a shallow understanding. Results of a multi-semester experiment to answer the following research questions: (1) With or without steps, can students learn the basics of tracing code on symbolic input values using an online tool? And how important is classroom instruction? (2) What is the impact of motivation on student attitudes in learning to reason with such a tool? Data was obtained from 297 subjects who used the online reasoning tool in a second-year software development course for CS majors. Analysis indicates that students can do symbolic reasoning to trace code and that instruction and motivation have significant impact.

Using freely available online automated reasoning tools, we will demonstrate a sequence of engaging reasoning activities that are suitable to introduce beginning programmers and software engineering students to reason logically and symbolically about code. The automated tools have an underlying verification engine that makes it possible for the tool to offer activities and directed logical feedback not possible with typical development environments. The tools have been used in undergraduate classrooms for multiple years by well over a thousand students. The imperative language used by the tool is integrated with the underlying verification engine, and because it closely resembles many commercial languages, it presents little barrier to student usage. A comprehensive activity-based "Reason with Components" tool takes 5-10 minutes of instructor introduction and allows student exploration of contracts, objects, loops, recursion, and reusable concepts. Multiple versions of "Begin to Reason" tools are designed to help students learn the basics of code tracing in intro CS courses "on their own". Students and instructors can create new activities and can fine-tune the existing activities to their specific needs.

In this BoF we discuss the tenets of culturally responsive computer science and how teachers, professors and providers of professional development can include culturally responsive perspectives in their classes. In contrast to other academic fields, which typically include rigid curricular tracks ostensibly based on academic performance, talent, or ability that pose structural barriers to access to rigorous academic instruction for underrepresented students, the field of computer science education is explicitly focused on broadening participation, as evidenced by the SIGCSE community's consistent emphasis on equitable representation. Culturally responsive computing (CRC) is founded on culturally responsive teaching (CRT) and on CRT's three tenets: asset building (in contrast to deficit approaches), reflection, and connectedness. CRC frames these tenets for the specifics of computing education. CRC's tenet that all students are capable of digital innovation should drive teachers' interactions and relationships with students. CRC also requires that teachers be continually reflective about their privilege and constraints and how those are connected with our worldviews. This topic is significant because teachers must be connected to their students in non-traditional ways that prize diversity as an asset to innovation. The participants are expected to include professors, lecturers, high school teachers and industry experts who are interested in employing culturally responsive computing approaches in their own teaching and professional development activities. A major goal of the BoF is to establish connections among the participants to promote the sharing of resources and best practices.

CS students can typically reason about what a piece of code does on specific inputs. While this is a useful starting point, graduates must also be able to logically analyze, comprehend, and predict the behavior of their code in more general terms, no matter what the inputs are. Results of data collection and analysis from an online educational system show it can help to pinpoint the difficulties in doing this for individual students and groups, and to partition the groups in terms of their difficulties so that instructional interventions may be better targeted. Unlike traditional debugging, this online system helps reveal difficulties in reasoning in more general terms because it is equipped with a verification engine.

You develop the prototype for a new learning strategy, and want to test it in class or across institutions. You identify an NSF program that supports proposals for the idea, and then what? What goes through the minds of reviewers once a proposal is submitted? What prompts one proposal to be recommended for funding while another is declined? Close examination of the panel review process can inform proposal writing and ensure that reviewers will understand a PI's idea, identify its merit, and value a PI's vision of how the work will broaden participation in STEM education. This workshop steps through the NSF proposal review process from submission of proposal to award or decline, touching on elements of a good review, NSF intellectual merit and broader impact criteria, elements of a good proposal, assessment and evaluation, and volunteering to review proposals. Participants gain insight into writing a good review and improving one's own proposal writing. The interactive workshop leads participants through each topic by introducing related issues, engaging participants in group exercises designed to explore and share their understanding of the issues, and providing "expert" opinion on these issues. Examples include funded and non-funded projects and a Top Ten List of Do's and Don'ts. For further information see: https://people.cs.clemson.edu/~etkraem/UPCSEd/

Analytical reasoning is central to code correctness, and every computer science curriculum aims to teach students how to achieve this objective in one form or another. With the acceptance of object-based computing and component-based software engineering, the need for analytical reasoning that is based on formal contracts to establish correctness of software across module boundaries has become ever more obvious. Yet there are few institutions that have integrated modular, analytical reasoning principles into their undergraduate curriculum. Among many reasons for this shortcoming are: the effort it takes overloaded faculty to integrate new ideas of any kind in their courses, the challenge of institutionalizing ideas within a specific context, and constraints of a particular college. This paper presents our experiences over nearly two decades at five different institutions with the hope that they will serve as useful curriculum examples for like-minded educators at other institutions.

This SIGCSE special session provides an opportunity for new researchers in CS education to learn the elements of successful computing education research of different types through a series of exemplar projects. Specifically, this session reports on the findings and example, successful CS education research projects that were discussed and presented at ICER 2016 UP (Understanding and Propagating) CS Ed Research Workshop, sponsored by the National Science Foundation. One goal of the session is to provide a way for proposers of computing education research to ensure that they have well identified education research questions and evaluation mechanisms that are appropriate for the proposal (exploratory vs. design & implementation) according to the Department of Education guidelines. The ICER Workshop was designed to focus exactly on this goal and report to the community.

Identification of an adequate invariant is valuable for reasoning about the correctness of code involving a loop, informally or formally. Almost every modern system for automated verification demands that programmers annotate their code with assertions, such as invariants to facilitate automation. But many learners struggle to grasp how to arrive at an assertion that remains an invariant and is sufficiently strong to prove subsequent assertions reliant on the outcome of the loop. The objective of this research is to present a method to help understand the difficulties students face in developing suitable loop invariants, and assist them in the process. We describe results from an experimentation in a software engineering classroom where students were charged with developing verified component-based code using a web-based front end for a verifying compiler. We collected data in the background as students attempted to produce verified code with loop invariants in in-class activities and take-home projects. Initial results show what kinds of information we can expect to see and what kinds of feedback might be useful.

Computing students often have difficulty understanding the relevance of the math we teach, though educators appreciate the significance. This BoF will discuss ways to connect this math with what computing students think they should be doing: programming. This BoF will focus on the benefits (and perils) of connecting math to the development of correct programs with the goal of motivating the relevance of the math-related portion of the ACM/IEEE Computer Society CS2013 curriculum. The discussion will continue the spirit and essence held by the math-thinking working group, a distributed working group of approximately 170 people who have been promoting and clarifying the importance of mathematics in computer science education.

A central goal of computer science education is to teach students how to reason about the correctness of the code they write. Typically, students use a trial and error process and check that their logic "works" by running it on test inputs. Typically, instructors encour-age them towards logical reasoning through manual tracing of the code. Rarely reasoning tools are used in the process, at least partly because few instructors are familiar with them and fewer have the time to investigate and experiment. The purpose of this panel is to introduce the attendees to a variety of reasoning tools the presenters have used in their classrooms. In some cases, the tools have been used in only one or two classes of a course to illustrate specific points. In other cases, entire projects have been done using the tools. The courses range from the introductory sequence and dis-crete structures to software engineering and graduate-level courses. The tools are freely available on the web and attendees will be encouraged to experiment with the reasoning tools on their own laptops to solve simple reasoning problems.

Undergraduate computer science students need to learn analytical reasoning skills to develop high-quality software and to understand why the software they develop works as specified. To accomplish this central educational objective, this article describes a systematic process of introducing reasoning skills into the curriculum and assessing how well students have learned those skills. To facilitate assessment, a comprehensive inventory of principles for reasoning about correctness that captures the finer details of basic skills that students need to learn has been defined and used. The principles can be taught at various levels of depth across the curriculum in a variety of courses. The use of a particular instructional process is illustrated to inculcate reasoning principles across several iterations of a sophomore-level development foundations course and a junior-level software engineering course. The article summarizes how learning outcomes motivated by the inventory of reasoning principles lead to questions that in turn form the basis for a careful analysis of student understanding and for fine-tuning teaching interventions that together facilitate continuous improvements to instruction.

Summary This paper summarizes our experiences over the last 4 years in creating a web‐integrated software development and verification environment. The environment has been used for both research experimentation and education. It has been used in undergraduate computer science courses to teach modular software development and analytical reasoning principles at multiple institutions. In the process, the environment has undergone many refinements to meet demands for improved functionality and to leverage rapidly changing underlying technology for the improvements. The environment is tailored to present formal specifications and alternative implementations of components, and enable correctness checking through a server‐side verifying compiler. This paper presents a detailed account of the development and evolution of the environment—its functionality, user interface, and underlying technology—that we hope will serve as a model for others, especially as the benefits of online learning systems are becoming increasingly obvious. Copyright © 2014 John Wiley & Sons, Ltd.

This paper summarizes our experiences integrating topics in the software development fundamentals (SDF), programming languages (PL), and software engineering (SE) knowledge areas of the ACM 2013 curriculum within a single course. It is novel in combining object-oriented programming and software development practices with fundamental analytical reasoning about software correctness. The aim is to integrate and cover the topics in an effective fashion. The course description in this paper represents an approach we have applied successfully for over 5 years. Students tend to consider this course to be one of the more challenging encountered in the first two years of study. Interestingly, the challenge appears to stem equally from mastering object-oriented programming and design pattern components of the course, as it does from learning to use specifications for analytical reasoning of component correctness.

SIGCSE has for a long time nourished an audience excited about teaching mathematical reasoning principles across the curriculum through the Math Thinking Birds-of-a-Feather session and panels on mathematical reasoning. While these forums are useful for discussing reasoning topics, they do not provide a consistent venue for sharing math-reasoning activities to be used in the classroom. Therefore, SIGCSE attendees interested in math thinking have routinely wished for a place for discussing engaging math reasoning examples and assignments. Providing such a forum is the purpose of this session. The exercises and assignments will help faculty find ways to incorporate mathematical reasoning in CS1, CS2, data structures and algorithms, discrete math, and software engineering courses.

Program correctness is central to computing, with instructors striving to convey the importance of getting it right starting in CS1. Teaching this material carefully demands a uniform framework to specify, implement, and reason about software correctness. To make these ideas accessible to educators and students, the tutorial will use RESOLVE, an integrated specification and programming language with a toolset especially designed for building verified components. The tutorial will also discuss how to get students involved through hands-on activities with software construction and modular verification using a web-integrated environment that requires no software installation and that features a prototype 'push-button' verifying compiler. The proposers have taught the ideas contained here using engaging pedagogical methods in introductory and advanced CS courses to thousands of students and dozens of educators over the past 20 years, and this SIGCSE tutorial will leverage that experience.

A key goal of our research is to introduce an approach that involves at the outset using analytical reasoning as a method for developing high quality software. This paper summarizes our experiences in introducing mathematical reasoning and formal specification-based development using a web-integrated environment in an undergraduate software engineering course at two institutions at different levels, with the goal that they will serve as models for other educators. At Alabama, the reasoning topics are introduced over a two-week period and are followed by a project. At Clemson, the topics are covered in more depth over a five-week period and are followed by specification-based software development and reasoning assignments. The courses and project assignments have been offered for multiple semesters. Evaluation of student performance indicates that the learning goals were met.

Is it possible to excite students about learning the mathematical principles that underlie high-quality software? Can they use a development environment for "hands-on" experimentation with reasoning? Is this possible without displacing existing content? The answer is a resounding yes "from the experiences of professors at several institutions" but it takes the right set of pedagogical principles, reasoning tools, and hands-on exercises. This laboratory will help educators transfer the excitement of learning how to apply mathematical reasoning in building high quality software, by adopting one reasoning concept at a time.

No abstract available.

This demonstration will present the RESOLVE web-integrated environment, which has been especially built to capture component relationships and allow construction and composition of verified generic components. The environment facilitates team-based software development and has been used in undergraduate CS education at multiple institutions. The environment makes it easy to simulate “what if” scenarios, including the impact of alternative specification styles on verification, and has spawned much research and experimentation. The demonstration will illustrate the issues in generic software verification and the role of higher-order assertions. It will show how logical errors are pinpointed when verification fails. Introductory video URL: http://www.youtube.com/watch?v=9vg3WuxeOkA.

The need for undergraduate CS students to create and understand mathematical abstractions is clear, yet these skills are rarely taught in a systematic manner, if they are taught at all. This paper presents a systematic approach to teaching abstraction using rigorous mathematical models and a web-based reasoning environment. It contains a series of representative examples with varying levels of sophistication to make it possible to teach the ideas in a variety of courses, such as introductory programming, data structures, and software engineering. We also present results from our experimentation with these ideas over a 3-year period at our institution in a required course that introduces object-based software development, following CS2.

Is it possible to excite students about learning the mathematical principles that underlie high-quality software? Can we teach them to apply these principles using modern software tools? Can this be accomplished without displacing existing content? In each case, the answer is a resounding yes - but it takes the right set of pedagogical principles, teaching tools, and classroom exercises. This hands-on laboratory will introduce a set of principles, tools, and exercises that have proven to work. By adopting one content module at a time, educators will better prepare students to reason rigorously about the software they develop and maintain.

No abstract available.

Abstract A central objective of the verifying compiler grand challenge is to develop a push-button verifier that generates proofs of correctness in a syntax-driven fashion similar to the way an ordinary compiler generates machine code. The software developer’s role is then to provide suitable specifications and annotated code, but otherwise to have no direct involvement in the verification step. However, the general mathematical developments and results upon which software correctness is based may be established through a separate formal proof process in which proofs might be mechanically checked, but not necessarily automatically generated. While many ideas that could conceivably form the basis for software verification have been known “in principle” for decades, and several tools to support an aspect of verification have been devised, practical fully automated verification of full software behavior remains a grand challenge. This paper explains how RESOLVE takes a step towards addressing this challenge by integrating foundational and practical elements of software engineering, programming languages, and mathematical logic into a coherent framework. Current versions of the RESOLVE verifier generate verification conditions (VCs) for the correctness of component-based software in a modular fashion—one component at a time. The VCs are currently verified using automated capabilities of the Isabelle proof assistant, the SMT solver Z3, a minimalist rewrite prover, and some specialized decision procedures. Initial experiments with the tools and further analytic considerations show both the progress that has been made and the challenges that remain.

No abstract available.

We introduce a "hands-on" experimentation approach for teaching mathematical specification and reasoning principles in a software engineering course. The approach is made possible by computer-aided analysis and reasoning tools that help achieve three central software engineering learning outcomes: (i) Learning to read specifications by creating test points using only specifications; (ii) Learning to use formal specifications in team software development while developing participating components independently; and (iii) Learning the connections between software and mathematical analysis by proving verification conditions that establish correctness for software components. Experimentation and evaluation results from two institutions show that our approach has had a positive impact.

We describe an approach to teaching formal interface specifications using aspects of the Collaborative Reasoning Paradigm. The module requires students to construct test cases independently and cooperatively based on their understanding of a given set of method specifications. Students are supported by software-based reasoning assistants that guide them through their exercises and provide realtime feedback as they work --- both for the students and the instructor. We describe the design of the course module, the supporting reasoning assistant, and representative reasoning exercises. We conclude with a discussion of evaluation results from a recent pilot study conducted at Clemson University.

The ultimate objective of a verifying compiler is to prove that proposed code implements a full behavioral specification. Experience reveals this to be especially difficult for programs that involve pointers or references and linked data structures. In some situations, pointers are unavoidable; in some others, verification can be simplified through suitable abstractions. Regardless, a verifying compiler should be able to handle both cases, preferably using the same set of rules. To illustrate how this can be done, we examine two approaches to full verification. One replaces language- supplied indirection with software components whose specifications abstract pointers and pointer- manipulation operations. Another approach uses abstract specifications to encapsulate data structures that pointers and references are often used to implement, limiting verification complications to inside the implementations of these components. Using a modular, specification-based tool we have developed for verification condition generation, we show that full verification of programs with and without the direct use of pointers can be handled similarly. There is neither a need to focus on selected pointer properties, such as the absence of null references or cycles, nor a need for special rules to handle pointers.

This roadmap describes ways that researchers in four areas---specification languages, program generation, correctness by construction, and programming languages---might help further the goal of verified software. It also describes what advances the "verified software" grand challenge might anticipate or demand from work in these areas. That is, the roadmap is intended to help foster collaboration between the grand challenge and these research areas.A common goal for research in these areas is to establish language designs and tool architectures that would allow multiple annotations and tools to be used on a single program. In the long term, researchers could try to unify these annotations and integrate such tools.

In design by contract (DBC), assertions are typically written using program variables and query methods. The lack of separation between program code and assertions is confusing, because readers do not know what code is intended for use in the program and what code is only intended for specification purposes. This lack of separation also creates a potential runtime performance penalty, even when runtime assertion checks are disabled, due to both the increased memory footprint of the program and the execution of code maintaining that part of the program's state intended for use in specifications. To solve these problems, we present a new way of writing and checking DBC assertions without directly referring to concrete program states, using ‘model’, i.e. specification-only, variables and methods. The use of model variables and methods does not incur the problems mentioned above, but it also allow one to write more easily assertions that are abstract, concise, and independent of representation details, and hence more readable and maintainable. We implemented these features in the runtime assertion checker for the Java Modeling Language (JML), but the approach could also be implemented in other DBC tools. Copyright © 2005 John Wiley & Sons, Ltd.

Two kinds of interface contract violations can occur in component-based software: A client component can fail to satisfy a requirement of a component it is using, or a component implementation can fail to fulfill its obligations to the client. The traditional approach to detecting and reporting such violations is to embed assertion checks into component source code, with compile-time control over whether they are enabled. This works well for the original component developers, but it fails to meet the needs of component clients who do not have access to source code for such components. A wrapper-based approach, in which contract checking is not hard-coded into the underlying component but is "layered" on top of it, offers several relative advantages. It is practical and effective for C++ classes. Checking code can be distributed in binary form along with the underlying component, it can be installed or removed without requiring recompilation of either the underlying component or the client code, it can be selectively enabled or disabled by the component client on a per-component basis, and it does not require the client to have access to any special tools (which might have been used by the component developer) to support wrapper installation and control. Experimental evidence indicates that wrappers in C++ impose-modest additional overhead compared to inlining assertion checks.

Summarizes an approach for introducing component-based software engineering (CBSE) early in the undergraduate computer science curriculum, and an evaluation of the impact of the approach at two institutions. Principles taught include a modular style of software development, an emphasis on human understanding of component behavior even while using formal specifications, and the importance of maintainability, as well as classical issues such as efficiency analysis and reasoning. Qualitative and quantitative evaluations of student outcomes and end-to-end changes in student attitudes show mostly positive results that are statistically significant, confirming that: (1) it is possible to teach CBSE principles without displacing "classical" principles usually taught in introductory courses, (2) students can understand and reuse formally specified components without knowing their implementations, and (3) student attitudes towards software engineering can be altered in directions heretofore often assumed to be difficult to achieve.

When teaching certain CS topics (e.g., abstract data types, operating systems), the instructor tries to make clear the distinction between the "client" perspective and the "implementer" perspective. But when teaching some programming language features and related programming techniques, this dichotomy often is not respected as strongly as it should be. We illustrate this with a discussion of how to teach recursion, comparing a traditional approach with one that is careful not to blur the distinctions between client view and implementer view. The latter better supports new learners in the creation of a sound and consistent mental model for developing and reasoning about programs that involve recursion.

Two kinds of interface contract violations can occur in component based software: a client component may fail to satisfy a requirement of a component it is using, or a component implementation may fail to fulfil its obligations to the client. The paper proposes a systematic approach for detecting both kinds of violations, so that violation detection is not hard coded into base level components, but is "layered" on top of them, and so that it can be turned "on" or "off" selectively for one or more components, with practically no change to executable code (limiting changes to a few declarations). Among the salient features of this approach are its use of formal specifications, the ability to handle parameterized (i.e., generic, or template) components, and the automatic generation of routine aspects of violation detection. We have designed, built, and experimented with a generator of checking components for C++ templates.

First-year computer science students need to see clearly that computer science as a discipline has an important intellectual role to play and that it offers deep philosophical questions, much like the other hard sciences and mathematics; that CS is not "just programming". An appropriate intellectual focus for CS1/CS2 can be built on the foundations of systems thinking and mathematical modeling, as these principles are manifested in a component-based software paradigm. We outline some of the main technical features of this approach to CS1/CS2 and report preliminary observations from our experience with it.

Object-based design and development are thought to facilitate graceful evolution of functionality, and thus enhance the reusability of software components. They can also facilitate graceful performance evolution. The performance of a layered object-based component can be made tunable to meet changing needs by permitting clients to ‘plug in’ appropriate implementations for its constituent components through generic parameters. If the components and their constituents are carefully designed, then performance tuning is possible without direct modification to the internal details of the participating components, thus significantly lowering the cost for performance evolution. The contribution of this paper is to software practice. It explains how software engineers can build performance-tunable components using C++ templates. It includes empirical results confirming that tuning produces expected performance improvements with minimal code change. The results are especially significant because they are scalable to arbitrarily large and heavily layered software components and subsystems. © 1997 by John Wiley & Sons, Ltd.

The typical correspondence between a concrete representation and an abstract conceptual value of an abstract data type (ADT) variable (object) is a many-to-one function. For example, many different pointer aggregates give rise to exactly the same binary tree. The theoretical possibility that this correspondence generally should be relational has long been recognized. By using a nontrivial ADT for handling an optimization problem, the authors show why the need for generalizing from functions to relations arises naturally in practice. Making this generalization is among the steps essential for enhancing the practical applicability of formal reasoning methods to industrial-strength software systems.

Abstract Different client applications of a given functional behaviour usually have different performance requirements. Designing a formal interface specification of the functional behaviour to allow for alternative implementations, and hence, to be suitable for clients with varying performance requirements, is a challenging task. The specifier must consider ramifications of alternative designs on performance to produce a truly implementation-neutral (and hence, performance-neutral) functionality specification. This paper illustrates the influence of performance-both duration and capacity — considerations using a case study in object-based software specification. When these considerations are combined with concerns for comprehensibility and full abstraction, specifications that result that are arguably among the most desirable.

Most modern designs of a software component include two separate pieces: functionality specification and implementation. When the specification is formal, this separation permits verification of reusable software components to be modular-essential for verification to be local, scalable, and hence, practical. In this paper, we explain the role of a third piece-an implementation dependent, performance specification-for a component. Introduction of this piece permits performance (e.g., execution time bonus) specification to be expressive (tight) while leaving functionality specification fully abstract and verification to be modular.>

For widespread reuse in a component-based software industry, a component must be designed and developed to be reused. Benefits of reuse are maximized when a component is reused “as is” (possibly with provisions for expected customization, such as through parameters), based only on its specification. The expression of the specification of a component is crucial in this setting. The specification must be formal, yet understandable, as well as abstract and implementation-independent. The specification also must make it possible to demonstrate correctness of an implementation of the specification and permit formal reasoning about its behavior in a client program. This paper explains how it is possible to write specifications with these properties in RESOLVE, a conceptual framework that we have developed for constructing reusable software components.

Current programming languages support construction of parameterized reusable components that can be adapted and composed to create new functionality. For widespread reuse, software components must also have readily adaptable performance. This paper introduces language mechanisms for creating such performance-parameterized reusable software components and for controlling their performance by "plugging in" appropriate constituent components. A key element of the proposed approach is that it provides inexpensive performance tuning. It permits performance of a tunable component to be changed without modifications to the functionality of the component or its clients; in principle, without the need for re-compilation or re-validation of functionality.