adding mutabelle as a component and an isabelle tool to be used in regression testing
authorbulwahn
Mon Dec 06 10:52:46 2010 +0100 (2010-12-06)
changeset 40975498f272b4bcb
parent 40974 29e5cae93584
child 40976 8df0a190df1e
adding mutabelle as a component and an isabelle tool to be used in regression testing
etc/components
src/HOL/Mutabelle/etc/settings
src/HOL/Mutabelle/lib/Tools/mutabelle
     1.1 --- a/etc/components	Mon Dec 06 10:52:45 2010 +0100
     1.2 +++ b/etc/components	Mon Dec 06 10:52:46 2010 +0100
     1.3 @@ -17,3 +17,4 @@
     1.4  src/HOL/Library/Sum_Of_Squares
     1.5  src/HOL/Tools/SMT
     1.6  src/HOL/Tools/Predicate_Compile
     1.7 +src/HOL/Mutabelle
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/HOL/Mutabelle/etc/settings	Mon Dec 06 10:52:46 2010 +0100
     2.3 @@ -0,0 +1,7 @@
     2.4 +MUTABELLE_HOME="$COMPONENT"
     2.5 +
     2.6 +MUTABELLE_LOGIC=HOL
     2.7 +MUTABELLE_IMPORT_THEORY=Complex_Main
     2.8 +MUTABELLE_OUTPUT_PATH=/tmp/mutabelle
     2.9 +
    2.10 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Mutabelle/lib/Tools/mutabelle	Mon Dec 06 10:52:46 2010 +0100
     3.3 @@ -0,0 +1,107 @@
     3.4 +#!/usr/bin/env bash
     3.5 +#
     3.6 +# Author: Lukas Bulwahn
     3.7 +#
     3.8 +# DESCRIPTION: mutant-testing tool for counterexample generators and automated proof tools
     3.9 +
    3.10 +
    3.11 +PRG="$(basename "$0")"
    3.12 +
    3.13 +function usage() {
    3.14 +  echo
    3.15 +  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
    3.16 +  echo
    3.17 +  echo "  Options are:"
    3.18 +  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
    3.19 +  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
    3.20 +  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
    3.21 +  echo
    3.22 +  echo "  THEORY is the name of the theory of which all theorems should be mutated and tested"
    3.23 +  exit 1
    3.24 +}
    3.25 +
    3.26 +
    3.27 +## process command line
    3.28 +
    3.29 +# options
    3.30 +
    3.31 +while getopts "L:T:O:t:q?" OPT
    3.32 +do
    3.33 +  case "$OPT" in
    3.34 +    L)
    3.35 +      MIRABELLE_LOGIC="$OPTARG"
    3.36 +      ;;
    3.37 +    T)
    3.38 +      MIRABELLE_IMPORT_THEORY="$OPTARG"
    3.39 +      ;;
    3.40 +    O)
    3.41 +      MIRABELLE_OUTPUT_PATH="$OPTARG"
    3.42 +      ;;
    3.43 +    \?)
    3.44 +      usage
    3.45 +      ;;
    3.46 +  esac
    3.47 +done
    3.48 +
    3.49 +shift $(($OPTIND - 1))
    3.50 +
    3.51 +[ "$#" -ne 1 ] && usage
    3.52 +
    3.53 +MUTABELLE_TEST_THEORY="$1"
    3.54 +
    3.55 +## main
    3.56 +
    3.57 +echo "Starting Mutabelle..."
    3.58 +
    3.59 +# setup
    3.60 +
    3.61 +mkdir -p "$MIRABELLE_OUTPUT_PATH"
    3.62 +
    3.63 +echo "theory Mutabelle_Test
    3.64 +imports $MUTABELLE_IMPORT_THEORY
    3.65 +uses     
    3.66 +  \"$MUTABELLE_HOME/mutabelle.ML\"
    3.67 +  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
    3.68 +begin
    3.69 +
    3.70 +ML {*
    3.71 +val mtds = [
    3.72 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"random\") \"random\",
    3.73 +  MutabelleExtra.quickcheck_mtd (Config.put Quickcheck.tester \"exhaustive\") \"exhaustive\"
    3.74 +]
    3.75 +*}
    3.76 +
    3.77 +ML {*
    3.78 +fun mutation_testing_of thy =
    3.79 +  (MutabelleExtra.random_seed := 1.0;
    3.80 +  MutabelleExtra.thms_of false thy
    3.81 +  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
    3.82 +         @{theory} mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
    3.83 +*}
    3.84 +
    3.85 +ML {*
    3.86 +  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
    3.87 +*}
    3.88 +
    3.89 +end" > $MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy
    3.90 +
    3.91 +# execution
    3.92 +
    3.93 +$ISABELLE_PROCESS -e 'use_thy "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test"' -q $MUTABELLE_LOGIC  > /dev/null 2>&1
    3.94 +
    3.95 +# make statistics
    3.96 +
    3.97 +GenuineCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: GenuineCex" | wc -l)
    3.98 +NoCex_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: NoCex" | wc -l)
    3.99 +Timeout_random=$(cat /$MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Timeout" | wc -l)
   3.100 +Errors_random=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_random: Error" | wc -l)
   3.101 +
   3.102 +GenuineCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: GenuineCex" | wc -l)
   3.103 +NoCex_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: NoCex" | wc -l)
   3.104 +Timeout_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Timeout" | wc -l)
   3.105 +Errors_exh=$(cat $MUTABELLE_OUTPUT_PATH/log | grep "quickcheck_exhaustive: Error" | wc -l)
   3.106 +
   3.107 +
   3.108 +echo "random      :" C: $GenuineCex_random N: $NoCex_random T: $Timeout_random E: $Errors_random
   3.109 +echo "exhaustive  :" C: $GenuineCex_exh N: $NoCex_exh T: $Timeout_exh E: $Errors_exh
   3.110 +