Lecture 10: Using SQL from Java

12 February 2009

SQL as a high-level declarative programming language. Domain-specific languages. Automated creation and manipulation of SQL. Example: SkyServer. Description of HTML injection and SQL injection. Accessing databases from programming languages: ODBC, JDBC, sample Java code for SQL queries. Demotion of SQL queries from structured programming to flat strings.

The lecture described handling SQL queries from Java. If your favourite programming language / framework does it differently (better?) then post details in the comments.

Read the rest of this entry »

Lecture 8: ESC/Java2

5 February 2009

ESC/Java2: a verification tool combining several analysis techniques (types, dataflow, proof). An overview of the checks it performs: exception freedom for common exceptions (null pointers, array indices, class casts). The lack of soundness and completeness: false positives and defects missed. Some further and specialised annotations extending core JML (non_null, unreachable, modifies, pure). Specification inheritance.

Read the rest of this entry »

Lecture 7: JML – the Java Modeling Language

2 February 2009

Review of Hoare logic.  Model-based specification as a technique for system design.  Design features of JML.  Some examples: preconditions, postconditions, invariants; model variables, methods and classes; ghost variables, assertions, assumptions.  JML as a common language across multiple tools for software specification and verification.

Read the rest of this entry »