Module 3: Software Specifications Flashcards

1
Q

key observations about specifications

A

specifications must be explicit
independent development and testing
resources are finite
program specs evolve over time

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
2
Q

testing

A

a form of consistency checking between implementation and spec

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
3
Q

black box testing

A

you see nothing about the program’s internal mechanisms

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
4
Q

white box testing

A

all program internal details are available

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
5
Q

grey box

A

between white and black box testing

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
6
Q

automated vs manual

A

automated:

  • find bugs more quickly
  • no need to write tests
  • if software changes, no need to maintain tests

manual

  • efficient
  • sometimes better coverage
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
7
Q

black box vs white

A

black

  • can work with code that cannot be modified
  • does not need to analyze or study code
  • can be performed in any format

white

  • efficient test suite
  • better coverage
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
8
Q

classification of specs

A

safety properties:

  • program will never reach a bad state
  • e.g. assertions, types, type-state properties

liveness properties:

  • program will eventually reach a good state
  • e.g. program terminations, starvation freedom
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
9
Q

common forms of safety properties

A

types: int x, java.net.Socket s, …

type-state properties: program must not read data from java.net.Socket until socket is connected

assertions: implicit, e.g. p != null before each dereference of p

pre and post conditions: double sqrt(double x) {…}
pre-condition: x >= 0
post-condition: return value ‘ret’ satisfies ret * ret = x

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
10
Q

types

A

adding the specification to the implementation allows to check the implementation against the specification

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
11
Q

checker framework

A

goal: statically eliminate entire classes of runtime errors via annotations

How well did you know this?
1
Not at all
2
3
4
5
Perfectly
12
Q

two kinds of useful invariant

A

loop invariant:

  • a property of a loop that holds before and after each iteration
  • captures the essence of the loop’s correctness, and by extension of algorithms that employ loops

class invariants:

  • a property that holds for all objects of a class
  • established upon the construction of the object and constantly maintained between calls to public methods
How well did you know this?
1
Not at all
2
3
4
5
Perfectly
13
Q

houdini algorithm

A
How well did you know this?
1
Not at all
2
3
4
5
Perfectly