Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: mutabelle Sprache: Isabelle

Original von: Isabelle^©

#!/usr/bin/env bash
#
# Author: Lukas Bulwahn
#
# DESCRIPTION: mutant-testing for counterexample generators and automated tools

PRG="$(basename "$0")"

function usage() {
  [ -n "$MUTABELLE_OUTPUT_PATH" ] || MUTABELLE_OUTPUT_PATH="None"
  echo
  echo "Usage: isabelle $PRG [OPTIONS] THEORY"
  echo
  echo "  Options are:"
  echo "    -L LOGIC     parent logic to use (default $MUTABELLE_LOGIC)"
  echo "    -T THEORY    parent theory to use (default $MUTABELLE_IMPORT_THEORY)"
  echo "    -O DIR       output directory for test data (default $MUTABELLE_OUTPUT_PATH)"
  echo "    -N NUMBER    number of lemmas to choose randomly, if not given all lemmas are chosen"
  echo "    -M NUMBER    number of mutants for each lemma (default $MUTABELLE_NUMBER_OF_MUTANTS)"
  echo "    -X NUMBER    number of mutations in a mutant  (default $MUTABELLE_NUMBER_OF_MUTATIONS)"
  echo
  echo "  THEORY is the name of the theory of which all theorems should be"
  echo "  mutated and tested."
  echo
  exit 1
}

## process command line

# options

MUTABELLE_IMPORTS=""

while getopts "L:T:O:N:M:X:" OPT
do
  case "$OPT" in
    L)
      MUTABELLE_LOGIC="$OPTARG"
      ;;
    T)
      MUTABELLE_IMPORTS="$MUTABELLE_IMPORTS \"$OPTARG\""
      ;;
    O)
      MUTABELLE_OUTPUT_PATH="$OPTARG"
      ;;
    N)
      NUMBER_OF_LEMMAS="$OPTARG"
      ;;
    M)
      MUTABELLE_NUMBER_OF_MUTANTS="$OPTARG"
      ;;
    X)
      MUTABELLE_NUMBER_OF_MUTATIONS="$OPTARG"
      ;;
    \?)
      usage
      ;;
  esac
done

shift $(($OPTIND - 1))

if [ "$MUTABELLE_IMPORTS" = "" ]
then
  MUTABELLE_IMPORTS="$MUTABELLE_IMPORT_THEORY"
fi

[ "$#" -ne 1 ] && usage

MUTABELLE_TEST_THEORY="$1"

if [ -z "$MUTABELLE_OUTPUT_PATH" ]; then
  MUTABELLE_OUTPUT_PATH="${ISABELLE_TMP_PREFIX}-mutabelle$$"
  PURGE_OUTPUT="true"
fi

export MUTABELLE_OUTPUT_PATH

if [ "$NUMBER_OF_LEMMAS" != "" ]; then
  MUTABELLE_FILTER="|> MutabelleExtra.take_random $NUMBER_OF_LEMMAS"
fi

## main

echo "Starting Mutabelle..."

# setup

mkdir -p "$MUTABELLE_OUTPUT_PATH"

echo "theory Mutabelle_Test
imports $MUTABELLE_IMPORTS
uses
  \"$MUTABELLE_HOME/mutabelle.ML\"
  \"$MUTABELLE_HOME/mutabelle_extra.ML\"
begin

declare [[quickcheck_timeout = 30]]

ML {*
val mtds = [
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"])) \"random\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"random\"]) #> Config.put Quickcheck.finite_types false) \"random_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"])) \"exhaustive\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"exhaustive\"]) #> Config.put Quickcheck.finite_types false) \"exhaustive_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types true) \"narrowing\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false) \"narrowing_int\",
  MutabelleExtra.quickcheck_mtd (Context.proof_map (Quickcheck.set_active_testers [\"narrowing\"]) #> Config.put Quickcheck.finite_types false
    #> Context.proof_map (Quickcheck.map_test_params (apfst (K [@{typ nat}])))) \"narrowing_nat\"
(*, MutabelleExtra.refute_mtd, *)
  , MutabelleExtra.nitpick_mtd

]
*}

ML {*
fun mutation_testing_of thy =
  (MutabelleExtra.random_seed := 1.0;
  MutabelleExtra.thms_of false thy $MUTABELLE_FILTER
  |> (fn thms => MutabelleExtra.mutate_theorems_and_write_report
         @{theory} ($MUTABELLE_NUMBER_OF_MUTATIONS, $MUTABELLE_NUMBER_OF_MUTANTS) mtds thms (\"$MUTABELLE_OUTPUT_PATH/log\")))
*}

ML {*
  mutation_testing_of @{theory $MUTABELLE_TEST_THEORY}
*}

end" > "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test.thy"

# execution

isabelle process -o auto_time_limit=10.0 \
  -T "$MUTABELLE_OUTPUT_PATH/Mutabelle_Test" -l "$MUTABELLE_LOGIC" > "$MUTABELLE_OUTPUT_PATH/err" 2>&1

[ $? -ne 0 ] && echo "isabelle processing of mutabelle failed"

# make statistics

function count() {
  cat "$MUTABELLE_OUTPUT_PATH/log" | grep "$1: $2" | wc -l | sed "s/     //"
}

function mk_stat() {
  printf "%-40s C:$(count $1 "GenuineCex")  P:$(count $1 "PotentialCex")  N:$(count $1 "NoCex")  T:$(count $1 "Timeout")  D:$(count $1 "Donno")  E: $(count $1 "Error")\n" "$1"
}

mk_stat "quickcheck_random"
mk_stat "quickcheck_random_int"
mk_stat "quickcheck_exhaustive"
mk_stat "quickcheck_exhaustive_int"
mk_stat "quickcheck_narrowing"
mk_stat "quickcheck_narrowing_int"
mk_stat "quickcheck_narrowing_nat"
##mk_stat "refute"
mk_stat "nitpick"

## cleanup

if [ -n "$PURGE_OUTPUT" ]; then
  rm -rf "$MUTABELLE_OUTPUT_PATH"
fi

¤ Dauer der Verarbeitung: 0.2 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.