Add propcheck tests

pubspec.yaml

@@ -11,4 +11,6 @@ dependencies:
   fixnum: ^0.10.5
 
 dev_dependencies:
+  enumerators: ^0.5.5
+  propcheck: ^0.5.1
   test: '>=0.12.0 <0.13.0'

test/bit_vector_test.dart

@@ -4,8 +4,17 @@
 import 'dart:math';
 
 import 'package:bit_vector/bit_vector.dart';
+import 'package:propcheck/propcheck.dart';
 import 'package:test/test.dart';
 
+import 'src/traces.dart';
+
+final Property implemMatchesModelProp = forall(programs, (program) {
+  return sameTraces(
+      program.execute(implFactory),
+      program.execute(modelFactory));
+});
+
 Random generator = new Random();
 
 BitVector makeVector(Iterable<int> elements) {
@@ -25,6 +34,16 @@ bool boolXor(bool x, bool y) => (x && !y) || (!x && y);
 
 void main() {
   group('BitVector', () {
+    test('quickcheck implem matches model', () {
+      final qc = new QuickCheck(maxSize: 500, seed: 42);
+      qc.check(implemMatchesModelProp);
+    });
+
+    test('smallcheck implem matches model', () {
+      final sc = new SmallCheck(depth: 7);
+      sc.check(implemMatchesModelProp);
+    });
+
     test('test []/set/clear/toggle', () {
       int failCount = 0;
       for (int i = 0; i < 100; i++) {

test/src/model.dart

@@ -0,0 +1,112 @@
+// Copyright (c) 2016, Kwang Yul Seo. All rights reserved. Use of this source code
+// is governed by a BSD-style license that can be found in the LICENSE file.
+
+import 'dart:math' show max;
+
+import 'package:bit_vector/bit_vector.dart' as impl;
+
+bool _isSet(bool b) => b;
+
+class BitVector implements impl.BitVector {
+  int _length;
+  List<bool> _bits;
+
+  BitVector([int length = 0])
+      : _bits = new List.filled(length, false, growable: true),
+        _length = length;
+
+  @override
+  bool get isEmpty => _length == 0;
+
+  @override
+  bool get isNotEmpty => _length != 0;
+
+  @override
+  int get cardinality => _bits.where(_isSet).length;
+
+  @override
+  int get length => _length;
+
+  @override
+  bool operator [](int bitIndex) {
+    if (bitIndex < 0)
+      throw new ArgumentError.value(bitIndex, 'bitIndex', 'bitIndex < 0');
+
+    return (bitIndex < _length) && _bits[bitIndex];
+  }
+
+  @override
+  void set(int bitIndex) {
+    if (bitIndex < 0)
+      throw new ArgumentError.value(bitIndex, 'bitIndex', 'bitIndex < 0');
+
+    _expandTo(bitIndex);
+    _bits[bitIndex] = true;
+  }
+
+  @override
+  void toggle(int bitIndex) {
+    if (bitIndex < 0)
+      throw new ArgumentError.value(bitIndex, 'bitIndex', 'bitIndex < 0');
+
+    _expandTo(bitIndex);
+    _bits[bitIndex] = !_bits[bitIndex];
+    _shrinkIfNecessary();
+  }
+
+  @override
+  void clear(int bitIndex) {
+    if (bitIndex < 0)
+      throw new ArgumentError.value(bitIndex, 'bitIndex', 'bitIndex < 0');
+
+    if (bitIndex >= _length) return;
+    _bits[bitIndex] = false;
+    _shrinkIfNecessary();
+  }
+
+  @override
+  void clearAll() {
+    while (_length > 0) {
+      _bits[--_length] = false;
+    }
+  }
+
+  @override
+  void and(BitVector other) => throw new UnimplementedError();
+
+  @override
+  void andNot(BitVector other) => throw new UnimplementedError();
+
+  @override
+  void or(BitVector other) => throw new UnimplementedError();
+
+  @override
+  void xor(BitVector other) => throw new UnimplementedError();
+
+  void _expandTo(int bitIndex) {
+    int lengthRequired = bitIndex + 1;
+    if (_length < lengthRequired) {
+      _ensureCapacity(lengthRequired);
+      _length = lengthRequired;
+    }
+  }
+
+  void _ensureCapacity(int lengthRequired) {
+    if (_bits.length < lengthRequired) {
+      // Allocate larger of doubled size or required size
+      int request = max(2 * _bits.length, lengthRequired);
+
+      int oldLength = _bits.length;
+      _bits.length = request;
+      _bits.fillRange(oldLength, _bits.length, false);
+    }
+  }
+
+  void _shrinkIfNecessary() {
+    int i;
+    for (i = _bits.length - 1; i >= 0; i--) {
+      if (_bits[i]) break;
+    }
+    _length = i + 1;
+  }
+}

test/src/traces.dart

@@ -0,0 +1,182 @@
+// Copyright (c) 2016, Kwang Yul Seo. All rights reserved. Use of this source code
+// is governed by a BSD-style license that can be found in the LICENSE file.
+
+import 'package:bit_vector/bit_vector.dart' as impl;
+import 'package:enumerators/combinators.dart' as co;
+import 'package:enumerators/enumerators.dart' as en;
+
+import 'model.dart' as model;
+
+abstract class BitVectorFactory {
+  impl.BitVector empty();
+}
+
+class _ImplFactory implements BitVectorFactory {
+  @override
+  impl.BitVector empty() => new impl.BitVector();
+}
+
+class _ModelFactory implements BitVectorFactory {
+  @override
+  impl.BitVector empty() => new model.BitVector();
+}
+
+final implFactory = new _ImplFactory();
+final modelFactory = new _ModelFactory();
+
+abstract class _ConstructorCall {
+  impl.BitVector execute(BitVectorFactory factory);
+}
+
+class _Empty extends _ConstructorCall {
+  _Empty();
+
+  String toString() => 'Empty()';
+
+  @override
+  impl.BitVector execute(BitVectorFactory factory) => factory.empty();
+}
+
+abstract class _Instruction {
+  _Result execute(impl.BitVector bv);
+}
+
+_Result _execute(f()) {
+  try {
+    return new _Value(f());
+  } catch (error) {
+    return new _Issue(error);
+  }
+}
+
+class _Set extends _Instruction {
+  final int i;
+  _Set(this.i);
+
+  @override
+  String toString() => 'Set($i)';
+
+  @override
+  _Result execute(impl.BitVector bv) => _execute(() => bv.set(i));
+}
+
+class _Get extends _Instruction {
+  final int i;
+  _Get(this.i);
+
+  @override
+  String toString() => 'Get($i)';
+
+  @override
+  _Result execute(impl.BitVector bv) => _execute(() => bv[i]);
+}
+
+class _Toggle extends _Instruction {
+  final int i;
+  _Toggle(this.i);
+
+  @override
+  String toString() => 'Toggle($i)';
+
+  @override
+  _Result execute(impl.BitVector bv) => _execute(() => bv.toggle(i));
+}
+
+class _Clear extends _Instruction {
+  final int i;
+  _Clear(this.i);
+
+  @override
+  String toString() => 'Clear($i)';
+
+  @override
+  _Result execute(impl.BitVector bv) => _execute(() => bv.clear(i));
+}
+
+class _ClearAll extends _Instruction {
+  _ClearAll();
+
+  @override
+  String toString() => 'ClearAll()';
+
+  @override
+  _Result execute(impl.BitVector bv) => _execute(() => bv.clearAll());
+}
+
+class _Program {
+  final _ConstructorCall constructorCall;
+  final List<_Instruction> instructions;
+  _Program(this.constructorCall, this.instructions);
+
+  @override
+  String toString() => 'Program($constructorCall, $instructions)';
+
+  List<_Result> execute(BitVectorFactory factory) {
+    final bv = constructorCall.execute(factory);
+    final result = [];
+    for (final instruction in instructions) {
+      result.add(instruction.execute(bv));
+    }
+    return result;
+  }
+}
+
+abstract class _Result {
+  bool same(_Result result);
+}
+
+class _Value extends _Result {
+  final Object value;
+
+  _Value(this.value);
+
+  @override
+  String toString() => 'Value($value)';
+
+  @override
+  bool same(_Result result) => result is _Value && value == result.value;
+}
+
+class _Issue extends _Result {
+  final Error error;
+
+  _Issue(this.error);
+
+  String toString() => 'Issue($error)';
+
+  bool same(_Result result) =>
+      result is _Issue && error.toString() == result.error.toString();
+}
+
+_empty() => new _Empty();
+
+final constructorCalls = en.singleton(_empty());
+
+_get(int i) => new _Get(i);
+_set(int i) => new _Set(i);
+_toggle(int i) => new _Toggle(i);
+_clear(int i) => new _Clear(i);
+_clearAll() => new _ClearAll();
+
+final instructions = en.apply(_get, co.ints) +
+    en.apply(_set, co.ints) +
+    en.apply(_toggle, co.ints) +
+    en.apply(_clear, co.ints) +
+    en.singleton(_clearAll());
+
+_program(_ConstructorCall constructorCall) =>
+    (List<_Instruction> instructions) =>
+        new _Program(constructorCall, instructions);
+
+final programs = en
+    .singleton(_program)
+    .apply(constructorCalls)
+    .apply(co.listsOf(instructions));
+
+bool sameTraces(List<_Result> trace1, List<_Result> trace2) {
+  if (trace1.length != trace2.length) return false;
+  for (var i = 0; i < trace1.length; i++) {
+    if (!trace1[i].same(trace2[i])) return false;
+  }
+  return true;
+}