CaseStudy2-modification.als

// CIS 623 - Case Study 2 / Spring 2013

sig char { }

// definite a file
sig File {
  stream : set char,	// file stream, the set of all chars
	firstChar : char & stream,	// the first character of a file
	lastChar : char & stream,		// the last character of a file
	nextChar : (stream - lastChar) -> one (char & stream),	// the next char of one char
	previousChar : (stream - firstChar) -> one (char & stream)	// the previous char of one char
} {
	stream = firstChar.*nextChar	// every char is the next char of some chars
	previousChar = ~nextChar	// previousChar is the inverse of nextChar
	nextChar in stream -> stream		// of course, every char is in the stream
}

// one's previous char cannot be its next char at the same time
pred example { }

run example for exactly 1 File, 4 char

// Delete the file or directory x
pred remove [f, f': File, x: char] {
	x in (f.stream - f.firstChar)
	f'.firstChar = f.firstChar
	f'.lastChar = f.lastChar
	f'.nextChar = f.nextChar - x->(x.(f.nextChar))
	f'.previousChar = f.previousChar - x->(x.(f.previousChar))
}

removeOkay: check {
	all f, f': File, x: char |
		remove[f, f', x] => f'.stream = f.stream - x
} for 5

run remove for 1 File, 4 char

CIS623_CaseStudy1.hs

{- This is case study 1 for CIS 623, by Kevin Wang, Spring 2013 -}

{- here we define the well-formed formula -}
data WFF = VAR String
  				| NEG WFF
					| AND WFF WFF
					| OR WFF WFF
					| IMPLY WFF WFF

{- here we define the WFF function, which is implemation free -}
iMPL_FREE	::	WFF				->	WFF
iMPL_FREE	(VAR p)			=		VAR p
iMPL_FREE	(NEG p)			=		NEG (iMPL_FREE p)
iMPL_FREE	(AND p q)		=		AND (iMPL_FREE p) (iMPL_FREE q)
iMPL_FREE	(OR p q)			=		OR (iMPL_FREE p) (iMPL_FREE q)
iMPL_FREE	(IMPLY p q)		=		OR (NEG (iMPL_FREE p)) (iMPL_FREE q)

{- this is the transform function -}
transform ::	WFF					->	WFF
transform (VAR p)				=		VAR p
transform (NEG (VAR p))		=		NEG (transform (VAR p))
transform (AND p q)			=		AND (transform p) (transform q)
transform (OR p q)				=		NEG (AND(NEG (transform p)) (NEG (transform q)))
transform (IMPLY p q)			=		NEG (AND (transform p) (NEG(transform q)))

{- here defines the NNF -}
nNF :: WFF							->	WFF
nNF (VAR p)						=		VAR p
nNF (OR p q)						=		OR (nNF p) (nNF q)
nNF (AND p q)					=		AND (nNF p) (nNF q)
nNF (NEG (NEG p))				=		nNF p
nNF (NEG (VAR p))				=		NEG (VAR p)
nNF (NEG (OR p q))				=		AND (nNF(NEG p)) (nNF(NEG q))
nNF (NEG (AND p q))			=		OR (nNF(NEG p)) (nNF(NEG q))

{- disjunction-free function -}
dISTR :: WFF		->	WFF	->	WFF
dISTR (AND n11 n12) n2		=		AND (dISTR n11 n2) (dISTR n12 n2)
dISTR n1 (AND n21 n22)		=		AND (dISTR n1 n21) (dISTR n1 n22)
dISTR p q								=		OR p q

{- the cNF function -}
cNF :: WFF 							->	WFF
cNF (VAR p)							=		VAR p
cNF (NEG p)						=		NEG p
cNF (AND p q)						=		AND (cNF p) (cNF q)
cNF (OR p q)						=		dISTR (cNF p) (cNF q)

{- a function used to show the WFF -}
instance	Show 	WFF	where
				show	(VAR p)			=	show p
				show	(NEG p)			=	"--"	++ show p
				show	(AND p q)		=	"("	++ show p ++	" ^ "		++ show q ++ ")"
				show	(OR p q)			=	"("	++ show p ++ " v "		++ show q ++ ")"
				show	(IMPLY p q)		=	"("	++ show p ++ " -> "	++ show q ++ ")"

{- here follows the test cases -}
case_IMPL1 = IMPLY (VAR "p") (VAR "q")
case_IMPL2 = AND (VAR "p") (VAR "q")
case_IMPL3 = OR (VAR "p") (VAR "q")

case_TRANS1 = IMPLY (VAR "p") (VAR "q")
case_TRANS2 = AND (VAR "p") (VAR "q")
case_TRANS3 = OR (VAR "p") (VAR "q")

case_NNF1 = NEG (NEG (VAR "p"))
case_NNF2 = NEG (AND (VAR "p") (VAR "q"))
case_NNF3 = NEG (OR (VAR "p") (VAR "q"))

case_CNF1 = NEG (VAR "p")
case_CNF2 = AND (VAR "p") (VAR "q")
case_CNF3 = OR (VAR "p") (VAR "q")