CS 2800 is a 4-credit course. The Office of the Registrar has useful information.

Sections

• Lecture: MWTh 1:35 - 2:40pm INV 019
• Lab 1: Fridays 13:35 - 14:25pm WVH 212
• Lab 2: Fridays 15:25 - 16:20pm WVH 212
• Lab 3: Fridays 16:20 - 17:10pm WVH 212

For information about the Instructor, TAs, and Tutors, click on Contact Info on your left.

You are required to check for announcements daily. Announcements will be made on piazza.

Rules

• If you don't understand something, please ask questions. We love questions. One of the benefits of attending a university as opposed to reading a book is that you get to interact with faculty.
• Give us feedback. Tell us what works; what doesn't. Tell us what you like about the class and what you don't like.
• In class, stay engaged during the lectures. We will have breaks and in-class exercises to break up the lectures but the course still covers a lot of potentially confusing material and you need to keep up. Therefore, the use of electronic devices (computers, recording devices, phones, etc) is not allowed unless it's for class. If you want to watch a cat video or play a video game (seriously: we've had this) then stay home.  I won't be upset and you won't be distracting people around you.
• We will be fair with everyone, so rest assured that all the students will play by the same rules. To that end, we have clear policies. Make sure you understand them, as they apply to everyone in the class. For example, late homeworks will not be accepted under any circumstances. If you ask us to make an exception for just you, the answer will be no. If you ask us to change the due date for everyone, then we will consider it. Please feel free to question the policies; if you suggest improvements, we can change our policies (and have done so in the past).

Books and Supplies

This term we are doing something a little different. Instead of the TurningPoint Responder Card RF (also referred to as the TurningPoint clicker) you may have heard previous sections used, we will be using Top Hat. This means the following:

1. You need to purchase a Top Hat license to take quizzes.  You should have already received an email about this. Talk to me if you encounter a problem.  Please sign up right away.  You won't be able to register later and still get marks for previous quizzes.  There is also a 2 week easy refund window if you take the class and drop it at the start of term.
   
2. This is a new technology for us. Please bear with me for technical issues and more importantly, please give me your feedback.
   
3. Each lecture you will need to bring your laptop, phone or tablet to class so you can take quizzes.  You should also install the Top Hat app on your phones.
   

There is no required book. If you want a reference that also includes a lot of exercises, then consider: Computer Aided Reasoning. Kaufmann, Manolios, Moore. You can order it from here. Please note that the book was written for at least upper level undergraduate students, so expect parts of the book to be hard. Also, in class we use a version of ACL2 that includes contracts and lots of other things that are not mentioned in the book. Nevertheless, this is the standard reference for ACL2 and contains many exercises whose solutions are available online.

Software

We will be using the ACL2s system. Please download it and install it on your machines. It is also installed in the CCIS computer labs, but there are some instructions you should follow to use that installation properly.

Academic Integrity

Read and intimately familiarize yourselves with the Northeastern Academic Integrity policy.

Please read and sign the Course Contract.

Warning: We do not tolerate any violations. If we suspect that you violated the policy, we will report you and the consequences can be as severe as expulsion from the university.

For example, here is something you cannot do, but again, read the full policy, the course contract and see Mitch Wand's Web page on the topic.

Unauthorized Collaboration: The University defines unauthorized collaboration as instances when students submit individual academic works that are substantially similar to one another. While several students may have the same source material, the analysis, interpretation, and reporting of the data must be each individual's independent work.

We will be using the clickers for quizzes. You can only use your clicker in class. If you use someone else's clicker, you are violating the academic integrity policy.

Exams

There are exactly two exams.Their times are:

• October 18, 6-8pm SH 335
  
• November 29, 6-8pm SH 335
  

If you can't make one of these exams, you need to contact me right away (and you need a good reason).

Grading

Grades will be determined as follows.

• Homeworks: 20%
• Exam 1 : 30%
• Exam 2 : 30%
• Quizzes : 20%

There are only 2 exams and there is no final.

Quizzes will occur regularly. Be prepared for a short quiz every day. Quizzes will utilize the Top Hat application. Only a subset of the quizzes might be graded. If you are not present for a quiz or if you forgot your phone, you will get 0 points. I would be surprised if someone forgot their laptop and phone but you never know. We will drop the lowest 10% of quizzes.

Homeworks will be given about once a week and due each Monday night at 11:59pm (although we can discuss changing that time). Your homework grade will be based on your top ten homeworks. You will mostly work in groups. We will give you instructions on group sizes and composition. We recommend that you to first try to solve the problems on your own. Then meet with your partners to go over your solutions and solve any unresolved problems. We may only grade a subset of the problems assigned.

You will spend most of your time in labs working on problems that we distribute in advance. If you solve the problems on your own before lab and are confident in your solutions, there is no need to show up. If you did not have time to solve the problems, or you tried and ran into trouble, then go to lab.

• You can take 1 double-sided sheet of paper to each exam.
• You have exactly 1 week after any assignment, quiz, or exam is graded to challenge your grade. After that, we will not change your grade.
• You are responsible for making sure that we entered the right points on Blackboard. If you notice any data entry errors, please inform us right away.

Prerequisites

CS 1800 and CS 2500.
If you do not have this background you should get the permission of the instructor. Our policy is that we do not grant exemptions. If you did not get passing grades in both the prerequisites: experience has shown that this is the best policy for students as the exception cases typically need to drop the course..

Schedule

It is important to remember that we can shift this schedule since this is a single section. Please point out any topics that you find extremely confusing or overwhelming (Equational Reasoning or Induction Schemes for example) and I can allocate extra class time for this.

Week	Topics
Sept 6 L1-L2	Introductions & motivation. Syllabus, class webpage, programming review Designing data-driven programs, the ACL2s development environment.
Sept 11 L3-L5	ACL2s development: Basic data types, expressions, syntax & semantics of atomic data and associated primitive functions Syntax & semantics of lists, design considerations of the ACL2s core language
September 18 L6-8	Contracts, termination, useful macros, let Datatypes: enumerated, range, product, record, union, list, (mutually) recursive Property-based testing, test?, program mode and defunc settings
September 25 L9-11	Property-based testing, test?, program mode and defunc settings. Catch up class. Boolean logic, one-time pads. Properties of Boolean operators, characterization of formulas, introduction to P=NP Proof methods: instantiation, case analysis, equational proofs, truth tables, decision procedures
October 2 L12-14	Limitations of Boolean logic, intro to equational reasoning for programs. Axioms for equality, cons-first-rest axioms, definitional axioms, instantiation, contract checking and completion. Equational reasoning in the presences of implications, context vs. theorems, undecidability results.
October 9 L15-16	Columbus Day (or Canadian Thanksgiving if you prefer): No classes Equational reasoning with nested Boolean Context. Reasoning about arithmetic, program equivalence: proving correctness of an exponential-time improvement, numeric reasoning in Java & other languages.
October 16 L17-19	The equational reasoning recipe and examples. More ER examples. Review for Exam 1 Definitions: soundness, termination, contracts, the ACL2s Definitional Principle.
October 23 L20-22	Termination and measure functions Using termination to show soundness of common recursions schemes and the design recipe, the undecidability of termination analysis, big-Oh analysis as a refinement of termination Proof by contradiction, mathematical induction, well-foundnesses, a proof that mathematical induction works, how to extract induction schemes from admissible recursive functions.
October 30 L23-25	Using induction to prove program correctness Induction like a professional Data-function-induction trinity
Nov 6 L26-28	Generalization, lemma generation, dealing with induction failure Intro to reasoning about accumulators Tail recursion: efficiency considerations, how to prove correctness
Nov 13 L29-31	Accumulator reasoning examples Abstract and algebraic data types
Nov 20 L32	Planning and structuring considerations for proofs Thanksgiving Break Thanksgiving Break
Nov 27 L33-35	Reasoning about algorithms & libraries: sorting, correctness Exam 2 Review Observational Equivalence
December 4 L36-37	Reasoning about imperative languages A look back: Logic and the birth of computer science; A look forward: what's next