Quelle Hashtable.vdmpp Sprache: VDM

/* Responsibility：
* Hash Table

* Usage：
* （１） Object in Hashtable have to have hashCode() function and equals() function.

* From historical reason, there are functional programming style and object-oriented style functions.
* if function name starts chapital letter, the function is functional programming style
* else the function is object-oriented style.
*/
class Hashtable is subclass of CommonDefinition

types
public Contents = map Object to Object;
public Bucket = map int to Contents;

instance variables
sBucket : Bucket := { |->};

operations

public Hashtable : () ==> Hashtable
Hashtable() ==
(
sBucket := { |-> };
return self
);

public Hashtable : Contents ==> Hashtable
Hashtable(aContents) ==
(
self.putAll(aContents);
return self
);

--Hashtableのクリアー
public clear : () ==> ()
clear() == setBuckets({ |-> });

public getBuckets : () ==> Bucket
getBuckets() == return sBucket;

public setBuckets : Bucket ==> ()
setBuckets(aBucket) == sBucket := aBucket;

public keySet : () ==> set of Object
keySet() ==
let buckets = self.getBuckets()
in
(
dcl allKeySet : set of Object := {};
for all aContents in set rng buckets do
  allKeySet := allKeySet union dom aContents;
return allKeySet
);

public put : Object * Object ==> ()
put(akey, aValue) ==
let buckets = self.getBuckets(),
  hashcode = akey.hashCode()
in
(
if hashcode in set dom buckets then
  self.setBuckets(buckets ++ {hashcode |-> (buckets(hashcode) ++ {akey |-> aValue})})
else
  self.setBuckets(buckets munion {hashcode |-> {akey |-> aValue}})
);

public putAll : Contents ==> ()
putAll(aContents) ==
for all key in set dom aContents do (
  self.put(key, aContents(key))
);

public get : Object  ==> [Object]
get(key) ==
let buckets = self.getBuckets(),
  hashcode = key.hashCode()
in
(
if hashcode in set dom buckets then
  let aContents = buckets(hashcode)
  in
  for all aKey in set dom aContents do (
   if key.equals(aKey) then
    return aContents(aKey)
  );
return nil
);

public remove : Object ==> [Object]
remove(key) ==
let buckets = self.getBuckets(),
  hashcode = key.hashCode(),
  deleteObj = self.get(key)
in
(
if deleteObj <> nil then
  let aContents = buckets(hashcode),
   newContents = aContents :-> {deleteObj}
  in
  (
  self.setBuckets(buckets ++ {hashcode |-> newContents});
  return deleteObj
  )
else
  return nil
);

public valueSet : () ==> set of Object
valueSet() ==
let buckets = self.getBuckets()
in
(
dcl aValueSet : set of Object := {};
for all aContents in set rng buckets do
  aValueSet := aValueSet union rng aContents;
return aValueSet
);

functions

public size : () -> nat
size() == card self.keySet();

public isEmpty : () -> bool
isEmpty() == self.keySet() = {};

public contains : Object -> bool
contains(anObject) ==
let buckets = self.getBuckets()
in
exists hashcode in set dom buckets &
  let aContents = buckets(hashcode)
  in
  exists key in set dom aContents &
    aContents(key).equals(anObject);

public containsKey : Object -> bool
containsKey(aKey) ==
let buckets = self.getBuckets()
in
exists hashcode in set dom buckets &
  exists key in set dom buckets(hashcode) &
   aKey.equals(key);

-----------Functional Programming part

functions

static public Put[@T1, @T2] :
(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> @T2
-> (map @T1 to (map @T1 to  @T2))
Put(aHashtable)(aHashCode)(aKey)(aValue) ==
let hashcode = aHashCode(aKey)
in
if hashcode in set dom aHashtable then
  aHashtable ++ {hashcode |-> (aHashtable(hashcode) ++ {aKey |-> aValue})}
else
  aHashtable munion {hashcode |-> {aKey |-> aValue}}
;

static public PutAll[@T1, @T2] :
(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2)
-> (map @T1 to (map @T1 to  @T2))
PutAll(aHashtable)(aHashCode)(aMap) ==
PutAllAux[@T1, @T2](aHashtable)(aHashCode)(aMap)(dom aMap);

static public PutAllAux[@T1, @T2] :
(map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> (map @T1 to  @T2)  -> set of @T1
-> (map @T1 to (map @T1 to  @T2))
PutAllAux(aHashtable)(aHashCode)(aMap)(aKeySet) ==
if aKeySet = {} then
  aHashtable
else
  let aKey in set aKeySet in
  let newHashtable = Put[@T1, @T2](aHashtable)(aHashCode)(aKey)(aMap(aKey))
  in
  PutAllAux[@T1, @T2](newHashtable)(aHashCode)(aMap)(aKeySet \ {aKey})
;

static public Get[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1  -> [@T2]
Get(aHashtable)(aHashCode)(aKey) ==
let hashcode = aHashCode(aKey)
in
if hashcode in set dom aHashtable then
  Map`Get[@T1, @T2](aHashtable(hashcode))(aKey)
else
  nil
;

static public Remove[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> (@T1 -> @T1) -> @T1 -> (map @T1 to (map @T1 to  @T2))
Remove(aHashtable)(aHashCode)(aKey) ==
let hashcode = aHashCode(aKey)
in
{h |-> ({aKey} <-: aHashtable(hashcode)) | h in set {hashcode}} munion
  {hashcode} <-: aHashtable ;

--Hashtableのクリアー
static public Clear[@T1, @T2] : () -> (map @T1 to (map @T1 to  @T2))
Clear() == ({ |-> });

static public KeySet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T1
KeySet(aHashtable) ==
--let aMapSet = rng aHashtable,
  --f = lambda x : map @T1 to  @T2 & dom x
let aMapSet = rng aHashtable
in
if aMapSet <> {} then
  --dunion Set`fmap[map @T1 to  @T2, @T2](f)(aMapSet)
  dunion  {dom s | s in set aMapSet}
else
  {};

static public ValueSet[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> set of  @T2
ValueSet(aHashtable) ==
--let aMapSet = rng aHashtable,
  --f = lambda x : map @T1 to  @T2 & rng x
let aMapSet = rng aHashtable
in
if aMapSet <> {} then
  --dunion Set`fmap[map @T1 to  @T2, @T2](f)(aMapSet)
  dunion  {rng s | s in set aMapSet}
else
  {};

static public Size[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> nat
Size(aHashtable) == card KeySet[@T1, @T2](aHashtable) ;

static public IsEmpty[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> bool
IsEmpty(aHashtable) == KeySet[@T1, @T2](aHashtable) = {};

static public Contains[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T2 -> bool
Contains(aHashtable)(aValue) ==
let aMapSet = rng aHashtable
in
if aMapSet <> {} then
  exists aMap in set aMapSet & aValue in set rng aMap
else
  false;

static public ContainsKey[@T1, @T2] : (map @T1 to (map @T1 to  @T2)) -> @T1 -> bool
ContainsKey(aHashtable)(aKey) ==
let aMapSet = rng aHashtable
in
if aMapSet <> {} then
  exists aMap in set aMapSet & aKey in set dom aMap
else
  false;

end Hashtable

quality95%

¤ Dauer der Verarbeitung: 0.18 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.