#!/bin/sh
# change-keywords -- change old-style JML keywords to new ones

USAGE='change-keywords.sh file1.java [file2.jml] ...'

# no arguments?
if test $# -eq 0
then
	echo "$USAGE" >&2
	exit 1
fi

for f
do
    mv $f ${f}.old || continue
    sed -e 's/\([^\\a-zA-Z_0-9]\)\(accessible\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(and\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(also\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(assert\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(assume\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(behavior\)\([^a-zA-Z_0-9]\)/\1\\normal \\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(by\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(callable\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(choose\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(constraint\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(decreasing\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(depends\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(ensures\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(everything\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(example\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(exists\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(forall\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(fresh\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(informally\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(initially\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(invariant\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(liberally\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(maintaining\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(measured\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(model\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(modifiable\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(nothing\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(old\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(on\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(or\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(program\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(pure\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(reach\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(redundantly\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(refine\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(represents\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(requires\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(result\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(returns\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(such\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(that\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(thrown\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(unmodified\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(weakly\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    s/\([^\\a-zA-Z_0-9]\)\(when\)\([^a-zA-Z_0-9]\)/\1\\\2\3/g
    ' ${f}.old > $f
done
