There has been debate about whether OO should, or even can, be taught first in CS1 (using Java). We claim that OO can be taught successfully, provided certain principles are followed. These principles lead to the requirement of an appropriate model for classes and objects, which we provide.

Teaching our students how to think about the programming process would increase our effectiveness as teachers and make our curriculum more efficient

CMS is a secure and scalable web-based course management system developed by the Cornell University Computer Science Department. The system was designed to simplify, streamline, and automate many aspects of the workflow associated with running a large course, such as course creation, importing students, management of student workgroups, online submission of assignments, assignment of graders, grading, handling regrade requests, and preparation of final grades. In contrast, other course management systems of which we are aware provide only specialized solutions for specific components, such as grading. CMS is increasingly widely used for course management at Cornell University. In this paper we articulate the principles we followed in designing the system and describe the features that users found most useful.

No abstract available.

No abstract available.

There are deep connections between algorithmic and mathematical thinking. Both construct "systems" --- computing systems in the algorithmic case, intellectual ones in mathematics --- from simple primitives. As Knuth notes in the preface to The Art of Computer Programming, "The construction of a computer program from a set of basic instructions is very similar to the construction of a mathematical proof from a set of axioms" [1]. Other connections include similar ways of organizing primitives into larger structures (e.g., recursion in algorithms, recursion and induction in math; conditionals in algorithms, definition in cases and proof by cases in math), similar ways of using abstraction to manage complexity, and an underlying reliance on logic. In short, mathematics is not merely a tool for limited areas of computer science, it is a mindset that fundamentally improves one's ability to devise and implement algorithms. Computer science students therefore need to exercise their mathematical as well as their computational abilities, and computer science educators need to help students use both ways of thinking to solve computing problems.This panel illustrates specific ways in which mathematical reasoning enhances algorithmic problem solving, and provides educators with concrete examples and resources to use in their own teaching. Each panelist will present an exercise, classroom example, or similar item, from their own experience, and will demonstrate ways in which mathematical reasoning helps one solve and/or understand it. The audience will be invited to contribute their own examples and to comment further on the role of mathematical thinking in computer science problem solving.The panelists' and audience members' examples will be collected on a Web page for continuing reference. A prototype of this page is at http://www.cs.geneseo.edu/~baldwin/math-thinking/examples.html.

In 1981 the APCS Development Committee recommended the use of Pascal in an AP course whose first exam was given in 1984. This decision was controversial; BASIC was in widespread use and serious consideration was given to a language-neutral exam and course. In 1985 an ad-hoc committee made recommendations on changing the exam format, essentially creating two courses that correspond roughly to CS1 and CS2. In 1995 an ad-hoc committee was convened to make recommendations on how best to incorporate C++ into the AP course and exam. The decision to adopt C++, made in 1994, was decidedly controversial. The ad-hoc committee made recommendations on a subset of C++ and on classes similar to those in the standard library, but which were safe for novice programmers to use.

Sound and complete modal propositional logic C is presented, in which □P has the interpretation ‘P is true in all states’. This interpretation is already known as the Camapian extension of S5. The new axiomatization for C provides two insights. First, introducing an inference rule textual substitution allows integration of the propositional and modal parts of the logic in a way that gives a more practical system for writing formal proofs. Second, the two following approaches to axiomatizing a logic are shown to be not equivalent: (i) give axiom schemes that denote an infinite number of axioms and (ii) write a finite number of axioms in terms of propositional variables and introduce a substitution inference rule.

We formalize the notion of underspecification as a means of avoiding problems with partial functions in modal logic S5 and some semantically related logics. For these logics, underspecification preserves validity, so incorporating it into their semantics leaves their classes of valid formulae unchanged.

No abstract available.

We formalize equational propositional logic, prove that it is sound and complete, and compare the equational-proof style with the more traditional Hubert style.

Communicating technical material orally is often hindered by the relentless linearity of audio; information flows actively past a passive listener. This is in stark contrast to communication through the printed medium, where we can actively peruse the visual display to access relevant information.

The relevance of formal methods for practical software system design is discussed. Prominent representatives of formal approaches present their findings and experience about the use and the usefulness of formal methods. It has been proposed that all programmers would be more productive and produce higher quality products if they would learn two things: predicate calculus; and program correctness (including formal program development). It is argued that the complexity, pervasiveness, and critical nature of modern and future computer systems makes it imperative that such systems be engineered for reliability and maintainability. Formal methods constitute an extremely promising approach to the design of reliable systems. The schedulability aspect of real-time system development is discussed. In general, formal methods should be preferred over other less formal methods since they can provide much better and stronger guarantees on real-time system performance.>

We consider incomplete trace-based network proof systems for safety properties, identifying extensions that are necessary and sufficient to achieve relative completeness. We investigate the expressiveness required of any trace logic to encode these extensions.

No abstract available.

It is ACM's 40th year and an old debate continues. Is computer science a science? An engineering discipline? Or merely a technology, an inventor and purveyor of computing commodities? What is the intellectual substance of the discipline? Is it lasting, or will it fade within a generation? Do core curricula in computer science and engineering accurately reflect the field? How can theory and lab work be integrated in a computing curriculum?We project an image of a technology-oriented discipline whose fundamentals are in mathematics and engineering — for example, we represent algorithms as the most basic objects of concern and programming and hardware design as the primary activities. The view that “computer science equals programming” is especially strong in our curricula: the introductory course is programming, the technology is in our core courses, and the science is in our electives. This view blocks progress in reorganizing the curriculum and turns away the best students, who want a greater challenge. It denies a coherent approach to making experimental and theoretical computer science integral and harmonious parts of a curriculum.Those in the discipline know that computer science encompasses far more than programming. The emphasis on programming arises from our long-standing belief that programming languages are excellent vehicles for gaining access to the rest of the field — but this belief limits out ability to speak about the discipline in terms that reveal its full breadth and richness.The field has matured enough that it is now possible to describe its intellectual substance in a new and compelling way. In the spring of 1986, ACM President Adele Goldberg and ACM Education Board Chairman Robert Aiken appointed this task force with the enthusiastic cooperation of the IEEE Computer Society. At the same time, the Computer Society formed a task force on computing laboratories with the enthusiastic cooperation of the ACM.The charter of the task force has three components: Present a description of computer science that emphasizes fundamental questions and significant accomplishments.Propose a new teaching paradigm for computer science that conforms to traditional scientific standards and harmoniously integrates theory and experimentation.Give at least one detailed example of a three-semester introductory course sequence in computer science based on the curriculum model and the disciplinary description.We immediately extended our task to encompass computer science and computer engineering, for we came to the conclusion that in the core material there is no fundamental difference between the two fields. We use the phrase “discipline of computing” to embrace all of computer science and engineering. The rest of this paper is a summary of the recommendation.The description of the discipline is presented in a series of passes, starting from a short definition and culminating with a matrix as shown in the figure. The short definition:Computer science and engineering is the systematic study of algorithmic processes that describe and transform information: their theory, analysis, design, efficiency, implementation, and application. The fundamental question underlying all of computing is, “What can be (efficiently) automated?”The detailed description of the field fills in each of the 27 cells in the matrix with significant issues and accomplishments. (That description occupies about 16 pages of the report.)For the curriculum model, we recommend that the introductory course consist of regular lectures and a closely coordinated weekly laboratory. The lectures emphasize fundamentals; the laboratories emphasize technology and know-how. The pattern of closely coordinated lectures and labs can be repeated where appropriate in other courses. The recommended model is traditional in the physical sciences and in engineering: lectures emphasize enduring principles and concepts while laboratories emphasize the transient material and skills relating to the current technology.

Abstract. Most trace-based proof systems for networks of processes are known to be incomplete. Extensions to achieve completeness are generally complicated and cumbersome. In this paper, a simple trace logic is defined and two examples are presented to show its inherent incompleteness. Surprisingly, both examples consist of only one process, indicating that network composition is not a cause of incompleteness. Axioms necessary and sufficient for the relative completeness of a trace logic are then presented.

The concept drift is a challenge in click fraud detection wherein frequent changes in the actual status label of publishers complicate the identification of publishers' fraudulent behavior. However, using transfer learning by leveraging the knowledge from previously learned domains to newer domains can make these differences more accessible while saving training time and improving the model's performance. But the absence of other user-click datasets available publicly poses complexity in using transfer learning. Therefore, to use transfer learning towards predicting the publisher's conduct concerning change in their labels, this work aims to transform 1D user-click non-image features into a 2D graphical image. The work proposes a deep convolution neural network-based transfer learning (DCNNTr) framework that utilizes different pre-trained Deep Convolutional Neural Network (DCNN) models as powerful feature extractors that leverage prior learnings to avert learning from scratch. The robust features extracted by the feature extractors help identify the conduct of publishers and classify them as fraudulent or non-fraudulent from 2D graphical images using machine learning models. By leveraging the weighted layers in extracting features, DCNN models utilize their special properties of being computationally efficient and locally focused. We evaluated the designed model on the FDMA2012 user-click dataset using precision, recall, F1-score, and AUC. Current work uniquely transforms the time series user-click non-image data into an image form. The experimental results demonstrate that features extracted with DenseNet121 followed by GTB have identified the fraudulent publishers with an average precision score of 79.8%.

A model and a sound and complete proof system for networks of processes in which component processes communicate exclusively through messages is given. The model, an extension of the trace model, can describe both synchronous and asynchronous networks. The proof system uses temporal-logic assertions on sequences of observations — a generalization of traces. The use of observations (traces) makes the proof system simple, compositional and modular, since internal details can be hidden. The expressive power of temporal logic makes it possible to prove temporal properties (safety, liveness, precedence, etc.) in the system. The proof system is language-independent and works for both synchronous and asynchronous networks.

The multiple assignment statement is defined in full generality—including assignment to subscripted variables and record fields—using the “axiomatic” approach of Hoare. Proof rules are developed for calls of procedures using global variables, var parameters, result parameters, and value parameters, using the idea of multiple assignment to provide understanding. An attempt is made to clarify some issues that have arisen concerning the use of rules of inference to aid in generating “verification conditions” in mechanical verifiers and the use of logical variables to denote initial values of program variables.

The “intermittent assertion” method for proving programs correct is explained and compared with the conventional method. Simple conventional proofs of iterative algorithms that compute recursively defined functions, including Ackermann's function, are given.

The conventional axiomatic definitions are given for multiple assignment to simple variables and for assignment to a single subscripted variable, along with examples to illustrate their use. The original contributions of this paper are the extension of the definition to include multiple assignment to several subscripted variables, and the development of a nontrivial, practical algorithm in which multiple assignment to several subscripted variables is indeed useful. Arguments are given to support the conjecture that the use of subscripted variables, like the use of pointers, can lead to exponential explosion of the length of a proof (and thus of the time needed to understand a program) unless the programmer is careful.

The ideas behind correctness proofs for programs are outlined, and conventional definitions of assignment, etc., are given. The main part of this paper is the idealized development of a nontrivial program in a disciplined fashion. The use of Dijkstra's "calculus" for the formal development of programs as a guide to structuring program development is discussed in relation to the example presented.

An introductory course (and its successor) in programming should be concerned with three aspects of programming:

We attempt to characterize classes of schemes allowing pushdown stores, building on an earlier work by Constable and Gries [1]. We study the effect (on the computational power) of allowing one, two, or more pushdown stores, both with and without the ability to detect when a pds is empty. A main result is that using one pds is computationally equivalent to allowing recursive functions. We also study the effect of adding the ability to do integer arithmetic, and multidimensional arrays.

We define the following classes of program schemata: ${\text{P}} = $ class of schemes using a finite number of simple variables; ${\text{P}}_{\text{A}} = $ class of schemes using simple and subscripted variables (arrays); ${\text{P}}_{{\text{Ae}}} = $ class of schemes in ${\text{P}}_{\text{A}} = $, with the addition of an equality test on subscript values; ${\text{P}}_{\text{R}} = $ class of schemes allowing recursive functions; ${\text{P}}_{\text{L}} = $ class of schemes allowing labels as values; ${\text{P}}_{\text{M}} = $ class of schemes allowing a finite number of special markers as values; ${\text{P}}_{{\text{pds}}} = $ class of schemes using pushdown stores. With these, we can also discuss, for example, ${\text{P}}_{{\text{AM}}} $, the class of schemes allowing arrays, and special markers as values ; and ${\text{P}}_{{\text{AL}}} $, the class of schemes allowing arrays, and labels as values. We argue that ${\text{P}}_{\text{A}}$, ${\text{P}}_{\text{R}}$, and ${\text{P}}_{\text{L}}$ faithfully represent mechanisms of subscripting, recursion, and labels as values, that are present in many “real” programming languages. We show that \[ {\text{P}} < {\text{P}}_{\text{R}} < {\text{P}}_{\text{A}} \equiv {\text{P}}_{{\text{AM}}} \equiv {\text{P}}_{{\text{pdsM}}} \equiv {\text{P}}_{{\text{Ae}}} \equiv {\text{EF}}, \] where EF is Strong’s class of effective functionals, assuming total functions and predicates. The inclusions ${\text{P}} < {\text{P}}_{\text{R}} < {\text{P}}_{\text{A}} $ and equivalences ${\text{P}}_{{\text{AL}}} \equiv {\text{P}}_{{\text{AM}}} \equiv {\text{P}}_{{\text{pdsM}}} \equiv {\text{P}}_{{\text{Ae}}} $ are effective. For example, given a program scheme in ${\text{P}}_{{\text{AM}}} $ we can construct an equivalent one in ${\text{P}}_{{\text{AL}}} $. However, we show that for any scheme in ${\text{P}}_{{\text{AM}}} $ an equivalent ${\text{P}}_{\text{A}} $ scheme exists, but also prove it cannot (in general) be constructed! We conjecture that ${\text{P}}_{{\text{A}}} $, ${\text{P}}_{{\text{AL}}} $, and equivalent classes are indeed “universal.” The above results assume that the uninterpreted functions and predicates are total. We discuss the problems which arise when they are partial. We define the class of multischemes and outline the relationship between the class ${\text{P}}_{{\text{Ae}}} $, multischemes, and Strong’s nondeterministic and deterministic effective functionals.